proposition: Lemma isometrie_egalite_module : forall (A B A' B' : PO) (z z' : C), distance A' B' = distance A B -> z = affixe_vec (vec A B) -> z' = affixe_vec (vec A' B') -> module z' = module z.
proof: Proof. intros A B A' B' z z'; try assumption. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros M; intros H1. elim existence_representant_vecteur with (A := O) (B := A') (C := B'); intros M'; intros H2. rewrite <- H2; rewrite <- H1; intros. rewrite (module_def2 (z:=z) (M:=M)); auto with geo. rewrite (module_def2 (z:=z') (M:=M')); auto with geo. rewrite (egalite_vecteur_distance (A:=O) (B:=M') (C:=A') (D:=B')); auto with geo. rewrite H; auto with geo. Qed.