proposition: Lemma cop2_onc6__eqc : forall A B C O P O' P', A <> B -> B <> C -> A <> C -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> OnCircle A O' P' -> OnCircle B O' P' -> OnCircle C O' P' -> Coplanar A B C O' -> EqC O P O' P'.
proof: Proof. intros A B C O P O' P'; intros. assert (HCong := onc2__cong O P). assert (HCong' := onc2__cong O' P'). assert (O = O') by (apply (cong4_cop2__eq A B C); Cong). apply eqc_chara. split. assumption. subst O'. apply cong_transitivity with O A; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel