proposition: Lemma conga_halfa__conga2 : forall P A O B P' A' O' B', HalfA P A O B -> HalfA P' A' O' B' -> CongA A O B A' O' B' -> CongA A O P A' O' P'.
proof: Proof. intros P A O B P' A' O' B' HP HP' HConga. apply sams2_suma2__conga with A O B. apply halfa__sams with B; assumption. apply halfa__suma; assumption. apply halfa__sams with B'; assumption. apply halfa__suma in HP'. assert_diffs. apply (conga3_suma__suma A' O' P' A' O' P' A' O' B'); CongA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma