proposition: Lemma pars__para : forall A B C D l m, IncidL A l -> IncidL B l -> IncidL C m -> IncidL D m -> Par_strict A B C D -> Para l m.
proof: Proof. intros A B C D l m HA HB HC HD [HCop HNI]. assert (A <> B) by (intro; subst; apply HNI; exists C; split; Col). assert (C <> D) by (intro; subst; apply HNI; exists A; split; Col). split. intros [X []]. apply HNI; exists X. rewrite 2 col_colh; split; [exists l|exists m]; repeat split; assumption. apply coplanar_plane in HCop. destruct HCop as [p]; spliter. exists p. split; [apply (line_on_plane A B)|apply (line_on_plane C D)]; assumption. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms