proposition: Lemma diff_nonzero : forall (a b : C) (A B : PO), a = affixe A -> b = affixe B -> A <> B :>PO -> Cplus b (Copp a) <> zeroC.
proof: Proof. intros. apply nonzero_module. rewrite (module_difference (a:=a) (b:=b) (A:=A) (B:=B)); auto with geo. Qed.