proposition: Lemma existence_mes_algebrique : forall (k : R) (A B : PO), exists C : PO, alignes A B C /\ mes_alg A C = k * mes_alg A B.
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); [ intros C H; try clear existence_representant_mult_vecteur; try exact H ]. exists C. cut (mes_alg A C = k * mes_alg A B); intros. split; [ idtac | try assumption ]. apply colineaire_alignes with k; auto. apply def_mes_alg; auto. Qed.