proposition: Lemma legendre_aux1 : greenberg_s_axiom -> triangle_postulate -> forall A1 A2 B1 B2 C1 C2 P, Perp2 A1 A2 B1 B2 P -> ~ Col A1 A2 P -> Col P B1 B2 -> Coplanar A1 A2 B1 B2 -> Par A1 A2 C1 C2 -> Col P C1 C2 -> ~ TS B1 B2 A1 C1 -> Col C1 B1 B2.
proof: Proof. intros greenberg triangle. intros A1 A2 B1 B2 C1 C2 P HPerp2 HNC HPB HCop HParAC HPC HNts. assert(HParAB : Par_strict A1 A2 B1 B2) by (apply (col_cop_perp2__pars_bis P); Col). apply (par_not_col_strict _ _ _ _ P) in HParAC; Col. elim(col_dec C1 B1 B2); auto. intro HC1NotB. exfalso. assert(P<>C1) by (intro; subst C1; Col). destruct HPerp2 as [P1 [P2 [HP [HPerpAP HPerpBP]]]]. assert(HQ := HPerpAP); auto. destruct HQ as [Q [_ [_ [HQP[HQA _]]]]]. assert(P<>Q) by (intro; subst Q; Col). apply (perp_col0 _ _ _ _ P Q) in HPerpAP; Col. apply (perp_col0 _ _ _ _ P Q) in HPerpBP; Col. clear dependent P1. clear dependent P2. assert_diffs. assert(Hos : OS B1 B2 Q C1). { apply (one_side_transitivity _ _ _ A1). - destruct (eq_dec_points A1 Q). subst A1; apply one_side_reflexivity; auto; apply (par_strict_not_col_2 A2); Par. apply l12_6, par_strict_right_comm, (par_strict_col_par_strict _ _ _ A2); Col; Par. - apply cop_nts__os; Col; [|apply (par_strict_not_col_2 A2); Par]. apply coplanar_pseudo_trans with A1 A2 P. assumption. apply coplanar_perm_1, col_cop__cop with B2; Col. apply coplanar_perm_1, col_cop__cop with B1; Col; Cop. Cop. apply coplanar_perm_1, col_cop__cop with C2; Col; Cop. } assert(~ Col Q C1 P) by (apply (par_not_col A1 A2); auto; apply par_strict_col_par_strict with C2; Col). assert(HQNotB : ~ Col B1 B2 Q) by (apply one_side_not_col123 with C1; auto). assert(HB3 : exists B3, Col B1 B2 B3 /\ OS P Q C1 B3). { destruct (col_dec P Q B1); [|apply cop_not_par_same_side with P; Col; apply coplanar_perm_12, coplanar_trans_1 with B2; Col; Cop]. assert (P = B1) by (apply (l6_21 B1 B2 Q P); Col). treat_equalities. destruct (cop_not_par_same_side P Q B2 P P C1) as [B3 []]; Col; Cop. exists B3; split; Col. } destruct HB3 as [B3 []]. assert(~ Col P Q B3) by (apply (one_side_not_col123 _ _ _ C1); Side). assert(HA3 : exists A3, Col A1 A2 A3 /\ OS P Q C1 A3). { assert (Coplanar A1 A2 C1 P) by (apply col_cop__cop with C2; Col; Cop). destruct (col_dec P Q A1); [|apply cop_not_par_same_side with Q; Col; apply coplanar_perm_5, col_cop__cop with A2; Col; Cop]. assert (Q = A1) by (apply (l6_21 A1 A2 P Q); Col). treat_equalities. destruct (cop_not_par_same_side P Q A2 Q Q C1) as [A3 []]; Col; Cop. exists A3; split; Col. } destruct HA3 as [A3 []]. assert_diffs. apply (legendre_aux greenberg triangle A3 B3 C1 P Q); trivial. apply (perp_col2 A1 A2); Col. apply (perp_col2 B1 B2); Col. apply (par_strict_col4__par_strict A1 A2 B1 B2); Col. apply (par_strict_col4__par_strict A1 A2 C1 C2); Col. apply (col2_os__os B1 B2); Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch13_1