proposition: Lemma t22_8__per : forall A B C D R S, Saccheri A B C D -> Bet B C R -> Bet A D S -> D <> S -> Per A S R -> Cong R S A B -> Per A B C.
proof: Proof. intros A B C D R S HSac HR HS HDS HPer HCong. assert(Hdiff := sac_distincts A B C D HSac). assert(HSac' := HSac). unfold Saccheri in HSac'. spliter. assert(B <> R) by (intro; treat_equalities; auto). assert(HSac' : Saccheri A B R S). { destruct (t22_8_aux A B C D R S R) as [_ []]; Cong. apply out_trivial; intro; treat_equalities; auto. } apply (per_col _ _ R); Col. apply (t22_7__per _ _ _ S C D); Perp; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma