proposition: Lemma Chasles_mes_alg : forall A B C : PO, alignes A B C -> mes_alg A B + mes_alg B C = mes_alg A C.
proof: Proof. intros. halignes H k. rewrite (mes_alg_conf (A:=B) (B:=B)); auto; ring. replace (mes_alg A B) with (1 * mes_alg A B). replace (mes_alg B C) with ((k + -1) * mes_alg A B). replace (mes_alg A C) with (k * mes_alg A B). ring. symmetry in |- *; apply def_mes_alg; auto. symmetry in |- *; apply def_mes_alg; auto. VReplace (vec B C) (add_PP (vec A C) (mult_PP (-1) (vec A B))). rewrite H0; Ringvec. symmetry in |- *; apply def_mes_alg; Ringvec. Qed.