proposition: Lemma image_distinct_centre : forall (I A B : PO) (a : R), I <> A :>PO -> B = rotation I a A :>PO -> I <> B :>PO.
proof: Proof. intros; red in |- *; intros. apply H. elim rotation_def with (I := I) (A := A) (B := B) (a := a); [ unfold distance in |- *; intros | auto | auto ]. rewrite <- H1 in H2. apply distance_nulle. rewrite <- (def_sqrt (scalaire (vec I A) (vec I A))); auto with geo. rewrite H2. replace (scalaire (vec I I) (vec I I)) with 0. rewrite sqrt_0; ring. replace (vec I I) with (mult_PP 0 (vec I B)). Simplscal. Ringvec. Qed.