proposition: Lemma zmult_char : forall (m n:nat) z, z = (m - n)%Z -> forall x, zmult x z [=] nmult x m[-]nmult x n.
proof: Proof. simple induction z; intros. simpl in |- *. replace m with n. Step_final ([0]:G). auto with zarith. simpl in |- *. astepl (nmult x (nat_of_P p)). apply cg_cancel_rht with (nmult x n). astepr (nmult x m). astepl (nmult x (nat_of_P p + n)). apply nmult_wd; algebra. rewrite <- convert_is_POS in H. auto with zarith. simpl in |- *. astepl [--](nmult x (nat_of_P p)). unfold cg_minus in |- *. astepr ([--][--](nmult x m)[+] [--](nmult x n)). astepr [--]([--](nmult x m)[+]nmult x n). apply un_op_wd_unfolded. apply cg_cancel_lft with (nmult x m). astepr (nmult x m[+] [--](nmult x m)[+]nmult x n). astepr ([0][+]nmult x n). astepr (nmult x n). astepl (nmult x (m + nat_of_P p)). apply nmult_wd; algebra. rewrite <- min_convert_is_NEG in H. auto with zarith. Qed.
imports: CoRN.algebra.CGroups