proposition: Lemma leP_trans : forall O E E' A B C, LeP O E E' A B -> LeP O E E' B C -> LeP O E E' A C.
proof: Proof. intros. unfold LeP in *. induction H; induction H0. left. unfold LtP in *. ex_and H dBA. ex_and H0 dCB. assert(Ar2 O E E' B A dBA). apply diff_ar2; auto. assert(Ar2 O E E' C B dCB). apply diff_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. assert(HH:= sum_exists O E E' H3 dBA dCB H10 H7). ex_and HH dCA. exists dCA. assert(HH:= sum_diff_diff_b O E E' A B C dBA dCB dCA H H0). split. apply HH. apply sum_comm; auto. apply(sum_pos_pos O E E' dBA dCB); auto. subst C. left; auto. subst B. left; auto. subst C. subst B. right; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod