proposition: Lemma double_Chasles : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> plus (double_AV (cons_AV (vec A B) (vec C D))) (double_AV (cons_AV (vec C D) (vec E F))) = double_AV (cons_AV (vec A B) (vec E F)) :>AV.
proof: Proof. unfold double_AV in |- *. intros. replace (plus (plus (cons_AV (vec A B) (vec C D)) (cons_AV (vec A B) (vec C D))) (plus (cons_AV (vec C D) (vec E F)) (cons_AV (vec C D) (vec E F)))) with (plus (plus (cons_AV (vec A B) (vec C D)) (cons_AV (vec C D) (vec E F))) (plus (cons_AV (vec A B) (vec C D)) (cons_AV (vec C D) (vec E F)))). rewrite Chasles; auto. mesure A B C D. mesure C D E F. replace (x + x0 + (x + x0)) with (x + x + (x0 + x0)); auto. ring. Qed.