proposition: Lemma halfa2_lea__lea1 : forall P A O B P' A' O' B', HalfA P A O B -> HalfA P' A' O' B' -> LeA A' O' P' A O P -> LeA A' O' B' A O B.
proof: Proof. intros P A O B P' A' O' B' HP HP' HLea. apply sams_lea2_suma2__lea with A' O' P' A' O' P' A O P A O P; trivial. apply halfa__sams with B; assumption. apply halfa__suma; assumption. apply halfa__suma; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma