proposition: Lemma cong4_cop2__eq : forall A B C P Q, A <> B -> B <> C -> A <> C -> Cong A P B P -> Cong A P C P -> Coplanar A B C P -> Cong A Q B Q -> Cong A Q C Q -> Coplanar A B C Q -> P = Q.
proof: Proof. intros A B C P Q; intros. assert (HNCol : ~ Col A B C) by (apply (cong2__ncol P); auto). destruct (eq_dec_points P Q); [assumption|]. exfalso. apply HNCol. assert (Haux : forall R, Col P Q R -> Cong A R B R /\ Cong A R C R). intros R HR; split; apply cong_commutativity, (l4_17 P Q); Cong. destruct (midpoint_existence A B) as [D]. assert_diffs. assert (HCol1 : Col P Q D). { assert (Coplanar A B C D) by Cop. apply cong3_cop2__col with A B; Cong; apply coplanar_pseudo_trans with A B C; Cop. } destruct (diff_col_ex3 P Q D HCol1) as [R1]; spliter. destruct (segment_construction R1 D R1 D) as [R2 []]. assert_diffs. assert (Col P Q R2) by ColR. destruct (Haux R1); trivial. destruct (Haux R2); trivial. assert (Cong A R1 A R2). { assert (Per A D R1) by (apply l8_2; exists B; split; Cong). apply l10_12 with D D; Cong. apply per_col with R1; ColR. } apply cong3_cop2__col with R1 R2; auto; [apply col_cop2__cop with P Q; auto..| |]. apply cong_transitivity with A R1; [|apply cong_transitivity with A R2]; Cong. apply cong_transitivity with A R1; [|apply cong_transitivity with A R2]; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2