proposition: Lemma l10_4 : forall A B P P', Reflect P P' A B -> Reflect P' P A B.
proof: Proof. intros. induction (eq_dec_points A B). subst B. unfold Reflect in *. elim H;intros. intuition. right. spliter. split. assumption. apply l7_2. assumption. rewrite -> (is_image_is_image_spec) in * by apply H0. apply l10_4_spec;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop