proposition: Lemma zmult_plus' : forall z x y, zmult x z[+]zmult y z [=] zmult (x[+]y) z.
proof: Proof. intro z; pattern z in |- *. apply nats_Z_ind. intro n; case n. intros; simpl in |- *. Step_final (([0]:G)[+]([0][-][0])). clear n; intros. rewrite POS_anti_convert; simpl in |- *. set (p := nat_of_P (P_of_succ_nat n)) in *. astepl (nmult x p[+]nmult y p). Step_final (nmult (x[+]y) p). intro n; case n. intros; simpl in |- *. Step_final (([0]:G)[+]([0][-][0])). clear n; intros. rewrite NEG_anti_convert; simpl in |- *. set (p := nat_of_P (P_of_succ_nat n)) in *. astepl ([--](nmult x p)[+] [--](nmult y p)). astepr [--](nmult (x[+]y) p). Step_final [--](nmult x p[+]nmult y p). Qed.
imports: CoRN.algebra.CGroups