proposition: Lemma t22_7__per : forall A B C D P Q, Saccheri A B C D -> Bet B P C -> Bet A Q D -> A <> Q -> Q <> D -> Per P Q A -> Cong P Q A B -> Per A B C.
proof: Proof. intros A B C D P Q HSac HP HQ HAQ HQD HPerQ HCong. assert(Hd := sac_distincts A B C D HSac). assert(HSac' := HSac). destruct HSac'. spliter. assert(B <> P). { intro. subst P. apply HAQ, (l8_7 B); trivial. apply per_col with D; Col. } assert(P <> C). { intro. subst P. apply HQD, (l8_7 C); apply per_col with A; Perp; Col. } assert(HSac1 : Saccheri A B P Q). { repeat split; Cong. apply (per_col _ _ D); Col. Perp. apply (col_one_side _ D); Col; apply (l9_17 _ _ C); Between. } assert(HSac2 : Saccheri D C P Q). { repeat split; auto. apply (per_col _ _ A); Col; Perp. apply (l8_3 A); Col; Perp. apply (cong_transitivity _ _ A B); Cong. apply (col_one_side _ A); Col. apply (l9_17 _ _ B); Between; Side. } apply (bet_suma__per _ _ _ B P C); auto. assert (P <> Q) by (intro; treat_equalities; auto). apply (conga3_suma__suma B P Q Q P C B P C); [SumA|..|CongA]. - apply (l11_10 B P Q A B P); Out. apply conga_sym, sac__conga, HSac1. - apply (conga_trans _ _ _ P C D). apply sac__conga, sac_perm, HSac2. apply (l11_10 B C D A B C); Out. apply conga_sym; apply sac__conga; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma