proposition: Lemma zero_plus_double : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> plus (image_angle 0) (double_AV (cons_AV (vec A B) (vec C D))) = double_AV (cons_AV (vec A B) (vec C D)) :>AV.
proof: Proof. intros. replace (image_angle 0) with (double_AV (cons_AV (vec A B) (vec A B))). rewrite double_Chasles; auto. unfold double_AV in |- *. rewrite <- angle_nul; auto. rewrite <- add_mes_compatible; auto. replace (0 + 0) with 0; auto. ring. Qed.