proposition: Lemma proclus_s_postulate_implies_strong_parallel_postulate : proclus_postulate -> strong_parallel_postulate.
proof: Proof. intros HP P Q R S T U HPTQ HRTS HNC1 HCop HCong1 Hcong2. unfold BetS in *; spliter. elim (col_dec P Q R); [exists P; split; ColR|intro HNC2]. destruct (HP P R Q S P U) as [I [HCol1 HCol2]]; [..|exists I; split]; Col. apply l12_17 with T; [assert_diffs|split..]; Cong. assert (Coplanar P Q R S) by (exists T; left; split; Col). CopR. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel