proposition: Lemma cop2_onc4__or_conga_suppa : forall O P A B C C', A <> B -> B <> C -> A <> C -> B <> C' -> A <> C' -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P -> Coplanar A B C O -> Coplanar A B C' O -> CongA A C B A C' B \/ SuppA A C B A C' B.
proof: Proof. intros O P A B C C'; intros. apply suma2__or_conga_suppa with A O B; trivial; apply inscribed_angle_1 with P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec