proposition: Lemma plg_not_comm : forall A B C D, A <> B -> Parallelogram A B C D -> ~ Parallelogram A B D C /\ ~ Parallelogram B A C D.
proof: Proof. intros. unfold Parallelogram. induction H0. split. intro. induction H1. apply plgs_not_comm in H0. spliter. contradiction. unfold Parallelogram_strict in H0. spliter. unfold Parallelogram_flat in H1. spliter. apply par_symmetry in H2. induction H2. unfold Par_strict in H2. spliter. apply H8. exists D; Col. spliter. unfold TS in H0. spliter. apply H0. Col. intro. assert(~ Parallelogram_strict A B D C /\ ~ Parallelogram_strict B A C D). apply plgs_not_comm. assumption. spliter. induction H1. contradiction. unfold Parallelogram_strict in H0. unfold Parallelogram_flat in H1. spliter. unfold TS in H0. spliter. contradiction. assert(~ Parallelogram_flat A B D C /\ ~ Parallelogram_flat B A C D). apply plgf_not_comm. assumption. assumption. spliter. split. intro. induction H3. unfold Parallelogram_strict in H3. unfold Parallelogram_flat in H0. spliter. unfold TS in H3. spliter. apply H3. Col. apply plgf_not_comm in H0. spliter. contradiction. assumption. intro. induction H3. unfold Parallelogram_strict in H3. unfold Parallelogram_flat in H0. spliter. unfold TS in H3. spliter. contradiction. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates