proposition: Lemma coplanar_trans_1 : forall P Q R A B, ~ Col P Q R -> Coplanar P Q R A -> Coplanar P Q R B -> Coplanar Q R A B.
proof: Proof. intros P Q R A B HNCol HCop1 HCop2. destruct (col_dec Q R A). exists A; left; split; Col. destruct (col_dec Q R B). exists B; left; split; Col. destruct (col_dec Q A B). exists Q; left; split; Col. assert (HDij : TS Q R A B \/ OS Q R A B). { assert (HA : TS Q R P A \/ OS Q R P A) by (apply cop__one_or_two_sides; Col; Cop). assert (HB : TS Q R P B \/ OS Q R P B) by (apply cop__one_or_two_sides; Col; Cop). destruct HA; destruct HB. - right; apply l9_8_1 with P; apply l9_2; assumption. - left; apply l9_2, l9_8_2 with P; assumption. - left; apply l9_8_2 with P; assumption. - right; apply one_side_transitivity with P; [apply one_side_symmetry|]; assumption. } destruct HDij; [apply ts__coplanar|apply os__coplanar]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar