proposition: Lemma halfa2_lea__lea2 : forall P A O B P' A' O' B', HalfA P A O B -> HalfA P' A' O' B' -> LeA A' O' B' A O B -> LeA A' O' P' A O P.
proof: Proof. intros P A O B P' A' O' B' HP HP' HLeA. assert (Hd := HP). apply halfa_distincts in Hd. assert (Hd' := HP'). apply halfa_distincts in Hd'. spliter. destruct (lea_total A O P A' O' P'); auto. apply conga__lea. apply conga_halfa__conga2 with B' B; [assumption..|]. apply lea_asym; [assumption|]. apply halfa2_lea__lea1 with P' P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma