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