((1 + (2 * 3), 4), 5)
: (nat * nat) * nat
mult_n_Sm =
fun n m : nat =>
nat_ind (fun n0 : nat => ((n0 * m) + n0) = (n0 * (S m)))
(eq_refl : ((0 * m) + 0) = (0 * (S m)))
(fun (p : nat) (H : ((p * m) + p) = (p * (S m))) =>
(let n0 := p * (S m) in
match H in (_ = n1) return (((m + (p * m)) + (S p)) = (S (m + n1))) with
| eq_refl =>
eq_ind (S ((m + (p * m)) + p))
(fun n1 : nat => n1 = (S (m + ((p * m) + p))))
(eq_S ((m + (p * m)) + p) (m + ((p * m) + p))
(nat_ind
(fun n1 : nat => ((n1 + (p * m)) + p) = (n1 + ((p * m) + p)))
(eq_refl : ((0 + (p * m)) + p) = (0 + ((p * m) + p)))
((fun (n1 : nat)
(H0 : ((n1 + (p * m)) + p) = (n1 + ((p * m) + p))) =>
f_equal_nat nat S ((n1 + (p * m)) + p)
(n1 + ((p * m) + p)) H0)
:
forall n1 : nat,
(((n1 + (p * m)) + p) = (n1 + ((p * m) + p))) ->
((((S n1) + (p * m)) + p) = ((S n1) + ((p * m) + p))))
m
:
((m + (p * m)) + p) = (m + ((p * m) + p))))
((m + (p * m)) + (S p)) (plus_n_Sm (m + (p * m)) p)
end)
:
(((S p) * m) + (S p)) = ((S p) * (S m)))
n
: forall n m : nat, ((n * m) + n) = (n * (S m))
Arguments mult_n_Sm (n m)%_nat_scope
1 :: (2 :: [3; 4])
: list nat
{0 = 1} + {2 <= (4 + 5)}
: Set
forall x y z : nat, [(x + y) + z] = [x + y + z]
: Prop
forall x y z : nat, [(x + y) + z] = [x + (y + z)]
: Prop
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
