proposition: Lemma tout_angle_mesure : forall a : AV, exists x : R, a = image_angle x :>AV.
proof: Proof. intros. elim existence_AB_unitaire; [ intros A H; elim H; [ intros B H0; try clear H existence_AB_unitaire; try exact H0 ] ]. elim existence_representant_cons with (a := a) (A := A) (B := B) (C := A); [ intros D H1; elim H1; [ intros H2 H3; try clear H1 existence_representant_cons; try exact H3 ] | auto ]. elim (tout_angle_a_une_mesure (A:=A) (B:=B) (C:=A) (D:=D)); auto with geo; intros. exists x. rewrite H4; auto. Qed.