proposition: Lemma sac_distincts : forall A B C D, Saccheri A B C D -> A <> B /\ B <> C /\ C <> D /\ A <> D /\ A <> C /\ B <> D.
proof: Proof. intros A B C D HSac. unfold Saccheri in HSac. spliter. assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto). assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side). assert_diffs. repeat split; auto. intro; treat_equalities. assert(A=D) by (apply (l8_7 B A D); Perp); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma