proposition: Lemma sum_preserves_lep : forall O E E' A B C AC BC, LeP O E E' A B -> Sum O E E' A C AC -> Sum O E E' B C BC -> LeP O E E' AC BC.
proof: Proof. intros. induction(eq_dec_points A B). { subst B. assert(HH:=sum_uniqueness O E E' A C AC BC H0 H1). subst BC. apply leP_refl. } { assert(LtP O E E' A B). { apply(lep_neq__ltp O E E' A B ); auto. } apply ltp_to_lep. apply (sum_preserves_ltp O E E' A B C AC BC); auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order