proposition: Lemma bet_leP : forall O E E' AB CD, Bet O AB CD -> LeP O E E' O AB -> LeP O E E' O CD -> LeP O E E' AB CD.
proof: Proof. intros. unfold LeP in *. induction H0; induction H1. unfold LtP in H0. unfold LtP in H1. ex_and H0 P. ex_and H1 Q. assert(Ar2 O E E' AB CD P /\ Col O E Q). unfold Diff in H0. ex_and H0 X. unfold Diff in H1. ex_and H1 Y. unfold Sum in H4. unfold Sum in H5. spliter. unfold Ar2 in *. spliter. repeat split; Col. unfold Ar2 in H4. spliter. assert(P = AB). apply (diff_uniqueness O E E' AB O); auto. apply diff_A_O; auto. subst P. assert(Q = CD). apply (diff_uniqueness O E E' CD O); auto. apply diff_A_O; auto. subst Q. clean_duplicated_hyps. induction(eq_dec_points AB CD). right. assumption. left. clear H0 H1. assert(HH:=opp_exists O E E' H4 AB H6). ex_and HH AB'. assert(exists P, Sum O E E' CD AB' P). apply(sum_exists O E E' H4 CD AB'); Col. unfold Opp in H0. unfold Sum in H0. spliter. unfold Ar2 in H0. tauto. ex_and H1 P. unfold LtP. exists P. split. unfold Diff. exists AB'. split; auto. assert(Diff O E E' CD AB P). unfold Diff. exists AB'. split; auto. apply diff_sum in H1. induction (eq_dec_points AB O). subst AB. unfold Ps in H2. unfold Out in H2. spliter. tauto. assert(Parallelogram_flat O AB CD P). apply (sum_cong O E E' H4 AB P CD H1). left. assumption. unfold Parallelogram_flat in H10. spliter. assert(Bet CD P O). apply(l4_6 O AB CD CD P O). assumption. repeat split; Cong. unfold Ps. unfold Out. repeat split. intro. subst P. assert(AB=CD). apply cong_symmetry in H13. apply (cong_identity _ _ O); Cong. subst CD. tauto. intro. subst E. apply H4. Col. unfold Ps in H3. unfold Out in H3. spliter. induction H17. left. apply (between_exchange4 O P CD E); Between. apply (l5_3 O P E CD); Between. subst CD. apply between_identity in H. subst AB. right; auto. subst AB. left; assumption. subst AB. subst CD. right; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order