proposition: Lemma cong_cop_per2_gen : 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 \/ Reflect X Y A B.
proof: Proof. intros. induction (cong_cop_per2 A B X Y H H0 H1 H2 H3). left; assumption. right. apply is_image_is_image_spec; assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity