proposition: Lemma ltP_sum_pos : forall O E E' A B C , Ps O E B -> Sum O E E' A B C -> LtP O E E' A C.
proof: Proof. intros. unfold LtP. exists B. split; auto. apply sum_diff in H0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod