proposition: Lemma t22_8_aux : forall A B C D R S J, Saccheri A B C D -> Bet B C R -> Bet A D S -> D <> S -> Per A S R -> Out S R J -> Cong S J A B -> C <> R /\ Saccheri A B J S /\ Saccheri D C J S /\ OS S J C B /\ Coplanar A B C J.
proof: Proof. intros A B C D R S J HSac HR HS HDS HPer HJ1 HJ2. assert(HSac' := HSac). unfold Saccheri in HSac'. spliter. assert_diffs. assert(HPar := sac__pars1423 A B C D HSac). assert(HPer1 : Per B A S) by (apply per_col with D; Col). assert(HPer2 : Per D S J) by (apply (l8_3 A); [apply per_col with R|..]; Col). assert(HPer3 : Per C D S) by (apply per_col with A; Perp; Col). assert(HOS : OS A S B J). { apply one_side_transitivity with R. apply col_one_side with D; Col; apply par_strict_one_side with C; Col. assert(~ Col A S R) by (apply per_not_col; auto). apply invert_one_side, out_one_side; Col. } assert(HSac' : Saccheri D C J S). { repeat split; auto. apply cong_transitivity with A B; Cong. apply one_side_transitivity with R. apply col_one_side with A; Col; apply par_strict_one_side with B; Par; Col. apply per_not_col in HPer2; auto; apply invert_one_side, out_one_side; Col. } assert(HNCol : ~ Col C J S) by (apply (par_strict_not_col_2 D), sac__pars1234, HSac'). assert(C <> R) by (intro; subst; apply HNCol; Col). repeat (split; try assumption). - apply per_col with R; Col. - Cong. - apply out_one_side_1 with R; [Col..|Out]. - apply coplanar_trans_1 with S. apply per_not_col; Perp. apply coplanar_perm_22, col_cop__cop with D; Col; Cop. Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma