blob: a5874f09a730b8f865f3775bdb7a7a1c049952ad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
((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
(fun (p : nat) (H : ((p * m) + p) = (p * (S m))) =>
let n0 := p * (S m) in
match H in (_ = y) return (((m + (p * m)) + (S p)) = (S (m + y))) 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
(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) m)) ((m + (p * m)) + (S p))
(plus_n_Sm (m + (p * m)) p)
end) n
: forall n m : nat, ((n * m) + n) = (n * (S m))
Arguments mult_n_Sm (_ _)%nat_scope
1 :: (2 :: [3; 4])
: list nat
{0 = 1} + {2 <= (4 + 5)}
: Set
|
