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