proposition: Lemma sum_preserves_ltp : forall O E E' A B C AC BC, LtP O E E' A B -> Sum O E E' A C AC -> Sum O E E' B C BC -> LtP O E E' AC BC.
proof: Proof. intros. apply ltp__lep_neq in H. spliter. apply lep_neq__ltp. split. apply(compatibility_of_sum_with_order O E E' A B C AC BC H H0 H1). intro. subst BC. assert(HS:= H0). unfold Sum in HS. unfold Ar2 in HS. spliter. clear H4. assert(A = B). { apply (sum_uniquenessA O E E' H3 C A B AC); auto. } contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order