proposition: Lemma t22_14__bet_aux : forall A B C P Q R, hypothesis_of_right_saccheri_quadrilaterals -> ~ Col A B C -> TriSumA A B C P Q R -> Acute A B C -> Acute A C B -> Bet P Q R.
proof: Proof. intros A B C P Q R rah HNCol HTri HacuteB HacuteC. apply trisuma_perm_312 in HTri. destruct HTri as [D [E [F []]]]. destruct (t22_14_aux A B C) as [A']; [assumption..|spliter]. assert_diffs. apply (bet_conga__bet B A' C); auto. apply (suma2__conga D E F B C A); auto. apply (suma_assoc B A' A C A A' _ _ _ _ _ _ _ _ _ A A' C); [..|SumA]. apply (conga2_sams__sams C A' A A' A C); CongA; SumA. apply (conga2_sams__sams A' A C A C A'); CongA; SumA. { apply suma_sym, (suma_assoc _ _ _ A' A B A B C _ _ _ C A B); auto. - apply os_ts__sams; Side. apply out_one_side; [Col|Out]. - apply (conga2_sams__sams A' A B A B A'); CongA; SumA. - SumA. - apply (conga3_suma__suma A' A B A B A' B A' A); CongA; apply t22_12__rah; auto. } apply (conga3_suma__suma A' A C A C A' C A' A); CongA; apply t22_12__rah; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma