proposition: Lemma halfa__suma : forall P A O B, HalfA P A O B -> SumA A O P A O P A O B.
proof: Proof. unfold HalfA. intros P A O B H. spliter. assert_diffs. apply (conga3_suma__suma A O P B O P A O B); [SumA|CongA..]. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma