proposition: Lemma module_difference : forall (a b : C) (A B : PO), a = affixe A -> b = affixe B -> module (Cplus b (Copp a)) = distance A B.
proof: Proof. intros. cut (Cplus b (Copp a) = affixe_vec (vec A B)); intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros D H2; intros; try exact H2. cut (Cplus b (Copp a) = affixe D); intros. rewrite (module_def (z:=Cplus b (Copp a)) (M:=D)); auto with geo. cut (Cplus b (Copp a) = affixe_vec (vec O D)); intros; auto with geo. rewrite H1; rewrite H2; auto. apply affixe_vec_AB; auto. Qed.