proposition: Lemma sac_plg : forall A B C D, Saccheri A B C D -> Parallelogram A B C D.
proof: Proof. intros A B C D H. assert (T:=sac__pars1234 A B C D H). assert (U:=sac__par1423 A B C D H). assert (V:=sac__par1234 A B C D H). apply par_2_plg;eauto using par_strict_not_col_1. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates