proposition: Lemma l10_10 : forall A B P Q P' Q', Reflect P' P A B -> Reflect Q' Q A B -> Cong P Q P' Q'.
proof: Proof. intros. induction (eq_dec_points A B). subst. unfold Reflect in *. induction H. intuition. induction H0. intuition. spliter. apply l7_13 with B; apply l7_2;auto. apply l10_10_spec with A B;try apply is_image_is_image_spec;assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity