proposition: Lemma ghalfa_out4__ghalfa : forall A B C D E F A' C' D' F', Out B A' A -> Out B C' C -> Out E D' D -> Out E F' F -> gHalfA A B C D E F -> gHalfA A' B C' D' E F'.
proof: Proof. intros A B C D E F A' C' D' F' HA HC HE HF HHalf. apply conga2_ghalfa__ghalfa with A B C D E F; [apply out2__conga..|]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma