proposition: Lemma le_right_comm : forall A B C D, Le A B C D -> Le A B D C.
proof: Proof. intros. induction(eq_dec_points D C). subst D. apply le_zero in H. subst B. eapply le_trivial. induction(eq_dec_points A B). subst B. apply le_trivial. assert(HH:=segment_construction_3 D C A B H0 H1). ex_and HH P'. unfold Out in H2. spliter. induction H5. assert(Le D C A B). eapply l5_5_2. exists P'. split; auto. apply le_left_comm in H6. assert(Cong A B C D). apply le_anti_symmetry. auto. auto. unfold Le. exists C. split. apply between_trivial. Cong. unfold Le. exists P'. split. assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec