proposition: Lemma sum_preserves_lep_rev : forall O E E' A B C AC BC, Sum O E E' A C AC -> Sum O E E' B C BC -> LeP O E E' AC BC -> LeP O E E' A B.
proof: Proof. intros. intros. assert(HS1:= H). assert(HS2:= H0). unfold Sum in HS1. unfold Sum in HS2. unfold Ar2 in *. spliter. clear H8. clear H3. unfold LeP in *. induction H1. { left. apply (sum_preserves_ltp_rev O E E' A B C AC BC); auto. } { subst BC. right. apply (sum_uniquenessA O E E' H7 C A B AC); auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order