proposition: Lemma plgf_trivial_trans : forall A B C, Parallelogram_flat A A B B -> Parallelogram_flat B B C C -> Parallelogram_flat A A C C \/ A = C.
proof: Proof. intros. induction(eq_dec_points A C). right. assumption. left. unfold Parallelogram_flat in *. spliter. repeat split; Col; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel