+theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ we proved (O = O) (trivial).
+ we proved (O = O ∨ m = O) (trivial2).
+ we proved (O*m=O → O=O ∨ m=O) (base_case).
+ (* inductive case *)
+ we need to prove
+ (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
+ (inductive_case).
+ assume n1: nat.
+ suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
+ (* base case *)
+ we proved (S n1 = O ∨ O = O) (pre_base_case2).
+ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+ (* inductive case *)
+ we need to prove
+ (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
+ (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
+ assume m1: nat.
+ suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
+ suppose (S n1 * S m1 = O) (absurd_hyp).
+ simplify in absurd_hyp.
+ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ we proved False (the_absurd).
+ we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O).
+ (* the induction *)
+ using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ done.
+ (* the induction *)
+ using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+done.
+qed.