proposition: Lemma gradaexp__grada : forall A B C D E F, GradAExp A B C D E F -> GradA A B C D E F.
proof: Proof. intros A B C. induction 1; [apply grada_init | apply grada2_sams_suma__grada with D E F D E F]; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel