proposition: Lemma image_sim_distinct_centre : forall (I A B : PO) (k a : R), I <> A -> k > 0 -> B = similitude I k a A -> I <> B.
proof: Proof. intros. elim similitude_def with (I := I) (A := A) (B := B) (k := k) (a := a); [ intros | auto | auto | auto ]. apply dist_non_nulle. rewrite H2. apply prod_neq_R0; auto with geo. auto with real. Qed.