proposition: Lemma out_preserves_halfa : forall P A O B P' A' B', Out O A A' -> Out O B B' -> Out O P P' -> HalfA P A O B -> HalfA P' A' O B'.
proof: Proof. intros P A O B P' A' B' HA HB HP [HNBet []]. apply l6_6 in HA. apply l6_6 in HB. apply l6_6 in HP. split; [|split]. intro; apply HNBet, bet_out_out_bet with A' B'; assumption. apply l11_25 with P A B; assumption. apply l11_10 with A P B P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma