proposition: Lemma zmult_plus : forall m n x, zmult x m[+]zmult x n [=] zmult x (m + n).
proof: Proof. intros; case m; case n; intros. simpl in |- *; Step_final ([0][+]([0][-][0]):G). simpl in |- *; Step_final ([0][+](nmult x (nat_of_P p)[-][0])). simpl in |- *; Step_final ([0][+]([0][-]nmult x (nat_of_P p))). simpl in |- *; Step_final (nmult x (nat_of_P p)[-][0][+][0]). simpl in |- *. astepl (nmult x (nat_of_P p0)[+]nmult x (nat_of_P p)). astepr (nmult x (nat_of_P (p0 + p))). rewrite nat_of_P_plus_morphism. apply nmult_plus. simpl (zmult x (Zpos p0)[+]zmult x (Zneg p)) in |- *. astepl (nmult x (nat_of_P p0)[+] [--](nmult x (nat_of_P p))). astepl (nmult x (nat_of_P p0)[-]nmult x (nat_of_P p)). apply eq_symmetric_unfolded; apply zmult_char with (z := (Zpos p0 + Zneg p)%Z). rewrite convert_is_POS. unfold Zminus in |- *. rewrite min_convert_is_NEG; auto. rewrite <- Zplus_0_r_reverse. Step_final (zmult x (Zneg p)[+][0]). simpl (zmult x (Zneg p0)[+]zmult x (Zpos p)) in |- *. astepl ([--](nmult x (nat_of_P p0))[+]nmult x (nat_of_P p)). astepl (nmult x (nat_of_P p)[+] [--](nmult x (nat_of_P p0))). astepl (nmult x (nat_of_P p)[-]nmult x (nat_of_P p0)). rewrite Zplus_comm. apply eq_symmetric_unfolded; apply zmult_char with (z := (Zpos p + Zneg p0)%Z). rewrite convert_is_POS. unfold Zminus in |- *. rewrite min_convert_is_NEG; auto. simpl in |- *. astepl ([--](nmult x (nat_of_P p0))[+] [--](nmult x (nat_of_P p))). astepl [--](nmult x (nat_of_P p0)[+]nmult x (nat_of_P p)). astepr [--](nmult x (nat_of_P (p0 + p))). apply un_op_wd_unfolded. rewrite nat_of_P_plus_morphism. apply nmult_plus. Qed.
imports: CoRN.algebra.CGroups