proposition: Lemma plgs_comm2 : forall A B C D, Parallelogram_strict A B C D -> Parallelogram_strict B A D C.
proof: Proof. intros. assert(HH:= H). apply plgs_two_sides in HH. spliter. unfold Parallelogram_strict in *. split. assumption. spliter. split. apply par_comm. assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates