proposition: Lemma par_par_cong_cong_parallelogram : forall A B C D, B<>D -> Cong A B C D -> Cong B C D A -> Par B C A D -> Par A B C D -> Parallelogram A B C D.
proof: Proof. intros. assert (Parallelogram A B C D \/ Parallelogram A B D C) by (apply par_cong_plg_2; assumption). assert (Parallelogram B C A D \/ Parallelogram B C D A) by (apply par_cong_plg_2; Cong). induction H4. assumption. induction H5. apply Plg_perm in H4. apply Plg_perm in H5. assert_diffs. spliter. apply plg_not_comm in H8. intuition. auto. apply Plg_perm in H5. spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates