proposition: Lemma plg_bet1 : forall A B C D, Parallelogram A B C D -> Bet A C B -> Bet D A C.
proof: Proof. intros. apply plg_col_plgf in H. unfold Parallelogram_flat in H. spliter. apply between_symmetry. apply (col_cong2_bet1 B). Col. Between. Cong. Cong. apply bet_col in H0. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel