proposition: Lemma grada2_sams_suma__grada : forall A B C D E F G H I K L M, GradA A B C D E F -> GradA A B C G H I -> SAMS D E F G H I -> SumA D E F G H I K L M -> GradA A B C K L M.
proof: Proof. intros A B C D E F G H I K L M HGA1 HGA2 HIsi. revert K L M. induction HGA2. { rename H into HConga; rename D0 into G; rename E0 into H; rename F0 into I. intros K L M HSuma. suma.assert_diffs. apply (conga2_sams__sams D E F G H I D E F A B C) in HIsi; CongA. apply (conga3_suma__suma D E F G H I K L M D E F A B C K L M) in HSuma; CongA. apply grada_stab with D E F; trivial. } assert (Hd1 := sams_distincts D0 E0 F0 A B C H0); assert (Hd2 := sams_distincts D E F G H I HIsi); spliter. destruct (ex_suma D E F D0 E0 F0) as [K [L [M HSuma]]]; auto. intros K0 L0 M0 HSuma2. assert (HIsi2 : SAMS D E F D0 E0 F0). apply sams_lea2__sams with D E F G H I; Lea. apply sams_suma__lea123789 with A B C; trivial. apply grada_stab with K L M. apply IHHGA2; trivial. apply sams_assoc_2 with D E F D0 E0 F0 G H I; trivial. apply suma_assoc_2 with D E F D0 E0 F0 G H I; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel