proposition: Lemma zmult_mult : forall m n x, zmult (zmult x m) n [=] zmult x (m * n).
proof: Proof. simple induction m; simple induction n; simpl in |- *; intros. Step_final ([0][-][0][+]([0]:G)). astepr ([0]:G). astepl (nmult ([0][-][0]) (nat_of_P p)). Step_final (nmult [0] (nat_of_P p)). astepr [--]([0]:G). astepl [--](nmult ([0][-][0]) (nat_of_P p)). Step_final [--](nmult [0] (nat_of_P p)). algebra. astepr (nmult x (nat_of_P (p * p0))). astepl (nmult (nmult x (nat_of_P p)) (nat_of_P p0)[-][0]). astepl (nmult (nmult x (nat_of_P p)) (nat_of_P p0)). rewrite nat_of_P_mult_morphism. apply nmult_mult. astepr [--](nmult x (nat_of_P (p * p0))). astepl ([0][-]nmult (nmult x (nat_of_P p)) (nat_of_P p0)). astepl [--](nmult (nmult x (nat_of_P p)) (nat_of_P p0)). rewrite nat_of_P_mult_morphism. apply un_op_wd_unfolded. apply nmult_mult. algebra. astepr [--](nmult x (nat_of_P (p * p0))). astepl (nmult [--](nmult x (nat_of_P p)) (nat_of_P p0)[-][0]). astepl (nmult [--](nmult x (nat_of_P p)) (nat_of_P p0)). rewrite nat_of_P_mult_morphism. eapply eq_transitive_unfolded. apply nmult_inv. apply un_op_wd_unfolded. apply nmult_mult. astepr (nmult x (nat_of_P (p * p0))). astepr [--][--](nmult x (nat_of_P (p * p0))). astepl ([0][-]nmult [--](nmult x (nat_of_P p)) (nat_of_P p0)). astepl [--](nmult [--](nmult x (nat_of_P p)) (nat_of_P p0)). rewrite nat_of_P_mult_morphism. apply un_op_wd_unfolded. eapply eq_transitive_unfolded. apply nmult_inv. apply un_op_wd_unfolded. apply nmult_mult. Qed.
imports: CoRN.algebra.CGroups