proposition: Lemma rah__posidonius_aux : postulate_of_right_saccheri_quadrilaterals -> forall A1 A2 A3 B1 B2 B3, Per A2 A1 B1 -> Per A1 A2 B2 -> Cong A1 B1 A2 B2 -> OS A1 A2 B1 B2 -> Col A1 A2 A3 -> Col B1 B2 B3 -> Perp A1 A2 A3 B3 -> Cong A3 B3 A1 B1.
proof: Proof. intros rah A1 A2 A3 B1 B2 B3 HPer1 HPer2 HCong HOS HA HB HPerp. assert (HSac : Saccheri A1 B1 B2 A2) by (repeat split; Perp; Cong). assert(Hdiff := sac_distincts A1 B1 B2 A2 HSac). spliter. assert_diffs. elim(eq_dec_points A1 A3). { intro. subst A3. assert(B1 = B3); [|subst; Cong]. apply (l6_21 B1 B2 A1 B1); Col. apply not_col_permutation_1, par_strict_not_col_1 with A2, sac__pars1234, HSac. unfold Saccheri in HSac; spliter; apply (cop_perp2__col _ _ _ A1 A2); Perp. apply col_cop__cop with B2; Cop. } intro. destruct(segment_construction_3 A3 B3 A1 B1) as [B'3 []]; auto. assert_diffs. assert(B3 = B'3); [|subst; assumption]. assert(Par_strict B1 B2 A1 A3). { apply (par_strict_col_par_strict _ _ _ A2); auto. apply par_strict_symmetry. apply sac__pars1423; assumption. } apply (l6_21 B1 B2 A3 B3); Col. apply (par_strict_not_col_4 _ _ A1); auto. apply col_permutation_2. assert (Coplanar A1 B2 B'3 B1). { apply coplanar_perm_15, coplanar_trans_1 with A3. apply not_col_permutation_2, par_strict_not_col_4 with A1; assumption. apply coplanar_perm_18, pars__coplanar; assumption. exists B3; right; right; split; Col. } apply cop_per2__col with A1; auto; apply l8_2. apply (rah _ _ _ A2); auto. apply (rah _ _ _ A3). unfold Saccheri in *. spliter. assert(B1 <> B3). { intro. subst B3. assert(A1 = A3); auto. apply (l8_18_uniqueness A1 A2 B1); Col; Perp. apply not_col_permutation_1; apply per_not_col; auto. } assert(Per A1 A3 B'3). { apply perp_per_1, perp_comm, (perp_col _ A2); Col. apply (perp_col1 _ _ _ B3); Col. } repeat split; Cong. apply (per_col _ _ A2); auto. apply (one_side_transitivity _ _ _ B3). apply l12_6; auto; apply (par_strict_col_par_strict _ _ _ B2); Col; Par. apply invert_one_side; apply out_one_side; auto; right; apply not_col_permutation_4; apply per_not_col; auto. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri