proposition: Lemma projete_non_axe : forall A B M H : PO, A <> B :>PO -> H = projete_orthogonal A B M :>PO -> ~ alignes A B M -> M <> H :>PO.
proof: Proof. intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=M) (H:=H)); auto; intros. red in |- *; intros; apply H2. rewrite H5; auto. Qed.