proposition: Lemma pi_plus_pi : image_angle deuxpi = image_angle 0.
proof: Proof. unfold deuxpi in |- *; intros. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. cut (A <> B); intros. rewrite add_mes_compatible. pattern (image_angle pi) at 1 in |- *. rewrite (angle_plat (A:=A) (B:=B)); auto. rewrite (angle_plat (A:=B) (B:=A)); auto. rewrite Chasles; auto. rewrite <- angle_nul; auto. auto with geo. Qed.