proposition: Lemma cong_cop_per2_1 : forall A B X Y, A <> B -> Per A B X -> Per A B Y -> Cong B X B Y -> Coplanar A B X Y -> X = Y \/ Midpoint B X Y.
proof: Proof. intros. eapply l7_20. apply col_permutation_5. apply (cop_per2__col A). Cop. assumption. apply l8_2. assumption. apply l8_2. assumption. assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity