proposition: Lemma projete_ortho_cote : forall A B C M P Q R : PO, triangle A B C -> triangle B C M -> triangle A B M -> triangle A C M -> P = projete_orthogonal B C M -> Q = projete_orthogonal A C M -> R = projete_orthogonal A B M -> double_AV (cons_AV (vec P Q) (vec P R)) = plus (double_AV (cons_AV (vec C A) (vec C M))) (double_AV (cons_AV (vec B M) (vec B A))) :>AV.
proof: Proof. intros A B C M P Q R H H0 H1 H2 H3 H4 H5. deroule_triangle A B C. deroule_triangle B C M. cut (M <> P); intros. elim (def_projete_orthogonal2 (A:=B) (B:=C) (C:=M) (H:=P)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=C) (C:=M) (H:=Q)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=M) (H:=R)); auto; intros. cut (P <> R); intros. cut (P <> Q); intros. replace (double_AV (cons_AV (vec P Q) (vec P R))) with (plus (double_AV (cons_AV (vec P Q) (vec P M))) (double_AV (cons_AV (vec P M) (vec P R)))). replace (double_AV (cons_AV (vec P Q) (vec P M))) with (double_AV (cons_AV (vec C A) (vec C M))). replace (double_AV (cons_AV (vec P M) (vec P R))) with (double_AV (cons_AV (vec B M) (vec B A))); auto. discrimine R B. rewrite (orthogonal_angles (A:=P) (B:=M) (C:=P) (D:=B)); auto. pattern B at 1 in |- *. rewrite <- H23. apply orthogonal_angles; auto with geo. red in |- *; intros; apply H10; rewrite <- H23; auto with geo. red in |- *; intros; apply H21; rewrite H23; auto with geo. apply orthogonal_alignement2 with C; auto with geo. replace (double_AV (cons_AV (vec B M) (vec B A))) with (double_AV (cons_AV (vec B M) (vec B R))). rewrite <- (def_opp (A:=P) (B:= R) (C:=P) (D:=M)); auto. rewrite double_opp; auto. rewrite <- (triangles_meme_hypotenuse (A:=M) (B:=B) (C:=R) (D:=P)); auto. rewrite <- double_opp; auto. rewrite def_opp; auto. apply orthogonal_alignement with A; auto. apply orthogonal_alignement2 with C; auto. apply alignement_et_angles; auto with geo. discrimine Q C. rewrite (orthogonal_angles (A:=P) (B:=C) (C:=P) (D:=M)); auto. pattern C at 2 in |- *. rewrite <- H23. apply orthogonal_angles; auto with geo. red in |- *; intros; apply H10; rewrite <- H23; auto with geo. red in |- *; intros; apply H22; rewrite H23; auto. apply ortho_sym. apply orthogonal_alignement with B; auto. replace (double_AV (cons_AV (vec C A) (vec C M))) with (double_AV (cons_AV (vec C Q) (vec C M))). rewrite <- (triangles_meme_hypotenuse (A:=M) (B:=C) (C:=Q) (D:=P)); auto. apply orthogonal_alignement with A; auto. apply orthogonal_alignement with B; auto. apply alignement_et_angles; auto with geo. rewrite double_Chasles; auto. apply non_alignes_distincts2 with M. deroule_triangle A C M. apply (triangle_ortho_cote (A:=A) (B:=B) (C:=C) (M:=M) (P:=P) (Q:=Q)); auto. apply non_alignes_distincts2 with M. deroule_triangle A B M. apply (triangle_ortho_cote2 (A:=A) (B:=B) (C:=C) (M:=M) (P:=P) (Q:=R)); auto. apply projete_non_axe with (2 := H3); auto. Qed.