proposition: Lemma Cop_aabc : forall A B C, Cop A A B C.
proof: Proof. intros A B C; assert (HE : forall A B C, A <> B -> Cop A A B C). { clear -TnEQD; intros A B C HAB. elim (col_dec A B C); intro HC; [destruct (not_col_exists A B) as [D]; auto|]; [exists A, B, D; repeat split; [|exists A..|exists B|exists C]; Col|]. exists A, B, C; repeat split; [|exists A..|exists B|exists A]; Col. } elim (eq_dec_points A B); intro; [|cut (Cop A A B C); [Copl|apply HE; auto]]. elim (eq_dec_points A C); intro; [|cut (Cop A A C B); [Copl|apply HE; auto]]. subst B; subst C; destruct (another_point A) as [B]. destruct (not_col_exists A B) as [C]; auto. exists A, B, C; repeat split; [|exists A..]; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.coplanar GeoCoq.Tarski_dev.Ch09_plane