proposition: Lemma conga_halfa__conga1 : forall P A O B P' A' O' B', HalfA P A O B -> HalfA P' A' O' B' -> CongA A O P A' O' P' -> CongA A O B A' O' B'.
proof: Proof. intros P A O B P' A' O' B' HP HP' HConga. apply (suma2__conga A O P A O P). apply halfa__suma; assumption. assert (Hd := HP'). apply halfa_distincts in Hd. spliter. apply (conga3_suma__suma A' O' P' A' O' P' A' O' B'); [|CongA..]. apply halfa__suma; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma