proposition: Lemma plg_par : forall A B C D, A <> B -> B <> C -> Parallelogram A B C D -> Par A B C D /\ Par A D B C.
proof: Proof. intros. assert(HH:= H1). apply plg_mid in HH. ex_and HH M. assert(HH:=l12_17 A B C D M H H2 H3). apply l7_2 in H2. assert(HH1:=l12_17 B C D A M H0 H3 H2). split. assumption. apply par_symmetry. Par. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates