proposition: Lemma halfa2_lta__lta1 : forall P A O B P' A' O' B', HalfA P A O B -> HalfA P' A' O' B' -> LtA A' O' P' A O P -> LtA A' O' B' A O B.
proof: Proof. intros P A O B P' A' O' B' HP HP' [HLea HNCong]. split. apply halfa2_lea__lea1 with P P'; assumption. intro. apply HNCong. apply conga_halfa__conga2 with B' B; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma