proposition: Lemma nonzero_diff : forall (a b : C) (A B : PO), a = affixe A -> b = affixe B -> Cplus b (Copp a) <> zeroC -> A <> B.
proof: Proof. intros. red in |- *; intros; apply H1. rewrite (affixe_vec_AB (a:=a) (b:=b) (A:=A) (B:=B)); auto. rewrite affixe_vec_AB_affixes; rewrite H2; ring. Qed.