proposition: Lemma triangles_meme_hypotenuse : forall A B C D : PO, A <> B -> B <> C -> A <> D -> C <> D -> orthogonal (vec C A) (vec C B) -> orthogonal (vec D A) (vec D B) -> double_AV (cons_AV (vec B C) (vec B A)) = double_AV (cons_AV (vec D C) (vec D A)) :>AV.
proof: Proof. intros. discrimine A C. rewrite <- angle_nul; auto. rewrite <- angle_nul; auto. discrimine B D. generalize (orthogonal_non_alignes (A:=C) (B:=A) (C:=B)); intros. generalize (orthogonal_non_alignes (A:=D) (B:=A) (C:=B)); intros. lapply (orthogonal_angles (A:=C) (B:=A) (C:=C) (D:=B)); auto; intros. lapply (orthogonal_angles (A:=D) (B:=A) (C:=D) (D:=B)); auto; intros. cut (triangle A B C); intros. cut (triangle A B D); intros. apply cocyclicite2; auto. apply reciproque_cocyclicite; auto. rewrite H9; auto; rewrite H10; auto. apply triangle_ordre_cycle; unfold triangle in |- *; auto. apply triangle_ordre_cycle; unfold triangle in |- *; auto. Qed.