proposition: Lemma acute_ghalfa2_sams_suma2__ghalfa456 : forall A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z', SAMS A' B' C' D' E' F' -> Acute D E F -> SumA A B C D E F X Y Z -> SumA A' B' C' D' E' F' X' Y' Z' -> gHalfA A B C A' B' C' -> gHalfA X Y Z X' Y' Z' -> gHalfA D E F D' E' F'.
proof: Proof. intros A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' HSams HAcute HSuma HSuma'. rewrite 3 ghalfa_chara. intros [HAcute1 HSuma1] [HAcute2 HSuma2]. split; [apply HAcute|]. assert_diffs. destruct (ex_suma D E F D E F) as [D'' [E'' [F'' HSuma3]]]; auto. apply (conga3_suma__suma D E F D E F D'' E'' F''); try apply conga_refl; auto. destruct (ex_suma A' B' C' D E F) as [G [H [I]]]; auto. assert (SumA A B C X Y Z G H I) by (apply suma_assoc_1 with A B C D E F A' B' C'; SumA). assert (SAMS A' B' C' D E F) by (apply sams_assoc_2 with A B C A B C X Y Z; SumA). apply sams2_suma2__conga456 with A' B' C' X' Y' Z'; trivial; clear dependent D'; clear dependent E'. apply sams_assoc_1 with D E F D E F G H I; [..|apply sams_assoc_2 with X Y Z A B C X Y Z]; SumA. apply suma_assoc_1 with D E F D E F G H I; [..|apply suma_assoc_2 with X Y Z A B C X Y Z]; SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma