proposition: Lemma sum_preserves_ltp_rev : forall O E E' A B C AC BC, Sum O E E' A C AC -> Sum O E E' B C BC -> LtP O E E' AC BC -> LtP O E E' A B.
proof: Proof. intros. assert(HS1:= H). assert(HS2:= H0). unfold Sum in HS1. unfold Sum in HS2. unfold Ar2 in *. spliter. clear H8. clear H3. assert(HH:= opp_exists O E E' H2 C H10). ex_and HH C'. assert (OP:=H3). unfold Opp in OP. unfold Sum in OP. unfold Ar2 in *. spliter. clear H12. unfold Opp in H3. apply sum_comm in H3; Col. assert(HH:= sum_exists O E E' H7 AC C' H11 H13). ex_and HH D. assert(HH:=sum_assoc O E E' A C C' AC O D H H3). destruct HH. assert(Sum O E E' A O D). { apply H17; auto. } assert(HS:=sum_A_O_eq O E E' H2 A D H18). subst D. assert(HH:= sum_exists O E E' H7 BC C' H6 H13). ex_and HH D. assert(HH:=sum_assoc O E E' B C C' BC O D H0 H3). destruct HH. assert(Sum O E E' B O D). { apply H21; auto. } assert(HS:=sum_A_O_eq O E E' H2 B D H22). subst D. apply(sum_preserves_ltp O E E' AC BC C' A B H1 H12 H19). Qed.
imports: GeoCoq.Tarski_dev.Ch14_order