proposition: Lemma triangle_ortho_cote : forall A B C M P Q R : PO, triangle A B C -> P = projete_orthogonal B C M -> Q = projete_orthogonal A C M -> ~ alignes A C M -> ~ alignes B C M -> ~ alignes M P Q.
proof: Proof. intros. deroule_triangle A B C. 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. lapply (projete_non_axe (A:=B) (B:=C) (M:=M) (H:=P)); auto; intros. lapply (projete_non_axe (A:=A) (B:=C) (M:=M) (H:=Q)); auto; intros. apply angle_non_alignes; auto. replace (double_AV (cons_AV (vec M P) (vec M Q))) with (double_AV (cons_AV (vec C B) (vec C A))). apply non_alignes_angle; auto with geo. rewrite (angles_droites_orthogonales (A:=C) (B:=B) (C:=C) (D:=A) (E:=M) (F:=P) (G:=M) (I:=Q)); auto with geo. Qed.