proposition: Lemma plgs_trans_trivial : forall A B C D B', Parallelogram_strict A B C D -> Parallelogram_strict C D A B' -> Parallelogram A B B' A.
proof: Proof. intros. apply plgs_permut in H. apply plgs_permut in H. assert (B = B'). eapply plg_uniqueness. left. apply H. left. assumption. subst B'. apply plg_trivial. apply plgs_diff in H. spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates