-intro.elim n
- [apply (ex_intro ? ? O).
- left.reflexivity
- |elim H. elim H1
- [apply (ex_intro ? ? a).
- right.apply eq_f.assumption
- |apply (ex_intro ? ? (S a)).
- left. rewrite > H2.
- apply sym_eq.
- apply times_SSO
- ]
- ]
-qed.
-
-theorem symmetric_times : symmetric nat times.
-unfold symmetric.
-intros.elim x
- [simplify.apply times_n_O.
- | simplify.rewrite > H.apply times_n_Sm.]
-qed.
-
-variant sym_times : \forall n,m:nat. n*m = m*n \def
-symmetric_times.
-
-theorem distributive_times_plus : distributive nat times plus.
-unfold distributive.
-intros.elim x.
-simplify.reflexivity.
-simplify.
-demodulate all.
-(*
-rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
-apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
-rewrite > assoc_plus.reflexivity. *)
-qed.
-
-variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
-\def distributive_times_plus.
-
-theorem associative_times: associative nat times.
-unfold associative.
-intros.
-elim x. simplify.apply refl_eq.
-simplify.
-demodulate all.
-(*
-rewrite < sym_times.
->>>>>>> .r9770
-rewrite > distr_times_plus.
-rewrite < sym_times.
-rewrite < (sym_times (times n y) z).
-rewrite < H.apply refl_eq.