proposition: Lemma t22_9_aux : forall N M P Q R S, Lambert N M P Q -> Lambert N M R S -> Bet M P R -> Bet N Q S -> (Per S R M <-> Per Q P M) /\ (Acute S R M <-> Acute Q P M).
proof: Proof. intros N M P Q R S HLamP HLamR HR HS. destruct(eq_dec_points Q S). { assert (HPar := lam__pars1234 N M P Q HLamP). unfold Lambert in *. spliter. treat_equalities. assert(P = R); [|subst; split; reflexivity]. apply (l6_21 M P Q P); Col. apply (par_strict_not_col_2 N), HPar. apply col_permutation_2, cop_per2__col with N; Perp. apply coplanar_perm_5, col_cop__cop with M; Col; Cop. } assert(HP' := symmetric_point_construction P M). destruct HP' as [P' HP']. apply l7_2 in HP'. assert(HQ' := symmetric_point_construction Q N). destruct HQ' as [Q' HQ']. apply l7_2 in HQ'. assert(HR' := symmetric_point_construction R M). destruct HR' as [R' HR']. apply l7_2 in HR'. assert(HS' := symmetric_point_construction S N). destruct HS' as [S' HS']. apply l7_2 in HS'. assert(HSacR := lam6534_mid2__sac S' R' R S M N HLamR HR' HS'). assert(HSacP := lam6534_mid2__sac Q' P' P Q M N HLamP HP' HQ'). assert(Cong S' R' R S /\ Cong Q' P' P Q) by (unfold Saccheri in *; spliter; split; auto). unfold Lambert in *. spliter. assert(HCongaR := sac__conga S' R' R S HSacR). assert(HCongaQ := sac__conga Q' P' P Q HSacP). assert(Bet P' P R) by (apply (outer_transitivity_between2 _ M); Between). assert(Bet Q' Q S) by (apply (outer_transitivity_between2 _ N); Between). assert(Bet R' P R) by (apply (between_exchange2 _ M); Between). assert(Bet S' Q S) by (apply (between_exchange2 _ N); Between). assert_diffs. assert(Per Q' S R) by (apply (l8_3 N); auto; ColR). assert(Per S' Q P) by (apply (l8_3 N); auto; ColR). assert(S' <> Q) by (intro; treat_equalities; auto). repeat split; intro. - apply (per_col _ _ P'); Col. apply (l11_17 Q' P' P); CongA. apply (t22_8__per _ _ _ Q R S); auto. apply cong_symmetry. apply (cong_transitivity _ _ S' R'); auto. apply (cong_transitivity _ _ P Q); auto. apply (t22_7__cong _ _ R S); Perp. apply (l11_17 S R R'); CongA. apply (per_col _ _ M); Col. - apply (per_col _ _ R'); Col. apply (l11_17 S' R' R); CongA. apply (t22_7__per _ _ _ S P Q); Perp. apply cong_symmetry. apply (cong_transitivity _ _ Q' P'); auto. apply (cong_transitivity _ _ R S); auto. apply (t22_8__cong _ _ P Q); auto. apply (l11_17 Q P P'); CongA. apply (per_col _ _ M); Col. - apply (acute_conga__acute Q' P' P). { apply (t22_8__acute _ _ _ Q R S); auto. apply (cong2_lt__lt P Q S' R'); Cong. apply (t22_7__lt5612 _ _ R S); Perp. apply (acute_conga__acute S R M); auto. apply (l11_10 S R R' S' R' R); [CongA|Out..]. } apply (l11_10 Q' P' P Q P P'); [CongA|Out..]. - apply (acute_conga__acute S' R' R). { apply (t22_7__acute _ _ _ S P Q); Perp. apply (cong2_lt__lt Q' P' R S); Cong. apply (t22_8__lt1256 _ _ P Q); auto. apply (acute_conga__acute Q P M); auto. apply (l11_10 Q P P' Q' P' P); [CongA|Out..]. } apply (l11_10 S' R' R S R R'); [CongA|Out..]. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma