proposition: Lemma similar__rah : postulate_of_existence_of_similar_triangles -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intro similar. destruct similar as [A [B [C [D [E [F]]]]]]. spliter. assert_diffs. elim (lea_total B C A A B C); auto; intro; [elim (le_cases D E A B)|elim (le_cases D F A C)]. - intro. apply (similar__rah_aux A B C D E F); auto. split; Cong. - intro. apply (similar__rah_aux D E F A B C); CongA. apply (ncol_conga_ncol A B C); auto. apply (l11_30 B C A A B C); auto. split; auto. - intro. apply (similar__rah_aux A C B D F E); Col; CongA. apply lea_comm; trivial. split; auto; intro; destruct(l11_50_1 A C B D F E); Col; CongA; Cong. - intro. apply (similar__rah_aux D F E A C B); CongA. apply (ncol_conga_ncol A C B); Col; CongA. apply (l11_30 A B C B C A); CongA. split; auto; intro; destruct(l11_50_1 A C B D F E); Col; CongA; Cong. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch12_parallel