proposition: Lemma plgs_in_angle : forall A B C D, Parallelogram_strict A B C D -> InAngle D A B C.
proof: Proof. intros. assert(Plg A B C D). apply parallelogram_to_plg. left. assumption. unfold Parallelogram_strict in H. unfold Plg in H0. spliter. ex_and H1 M. assert(A <> B /\ C <> B). unfold TS in H. spliter. split; intro; subst B; apply H; Col. spliter. assert(HH:=H). unfold TS in HH. spliter. ex_and H9 T. unfold InAngle. repeat split; auto. intro. subst D. apply l7_3 in H4. subst M. apply midpoint_bet in H1. apply H7. apply bet_col in H1. Col. exists M. split. apply midpoint_bet. auto. right. unfold Out. repeat split. intro. subst M. unfold Midpoint in H4. spliter. apply cong_symmetry in H11. apply cong_identity in H11. subst D. apply between_identity in H10. subst T. contradiction. intro. subst D. apply between_identity in H10. subst T. contradiction. left. apply midpoint_bet. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates