proposition: Lemma plgs_not_comm : forall A B C D, Parallelogram_strict A B C D -> ~ Parallelogram_strict A B D C /\ ~ Parallelogram_strict B A C D.
proof: Proof. intros. unfold Parallelogram_strict in *. split. intro. spliter. assert(HH:= ts_cong_par_cong_par A B C D H H4 H3). spliter. assert(Par_strict A D C B). induction H6. assumption. spliter. unfold Par_strict. repeat split; Cop. intro. unfold TS in *. spliter. apply H. Col. apply l12_6 in H7. apply l9_9 in H0. apply one_side_symmetry in H7. contradiction. intro. spliter. assert(HH:=ts_cong_par_cong_par A B C D H H4 H3). spliter. apply par_symmetry in H6. assert(Par_strict C B A D). induction H6. assumption. spliter. unfold Par_strict. repeat split; Cop. intro. unfold TS in *. spliter. apply H13. Col. apply l12_6 in H7. apply l9_9 in H0. apply invert_one_side in H7. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates