variant distr_Ztimes_Zplus: \forall x,y,z.
x * (y + z) = x*y + x*z \def
distributive_Ztimes_Zplus.
-
-theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
-Z_of_nat n + Z_of_nat m.
-intro.cases n;intro
- [reflexivity
- |cases m
- [simplify.rewrite < plus_n_O.reflexivity
- |simplify.reflexivity.
- ]]
-qed.