proposition: Lemma grada__lea : forall A B C D E F, GradA A B C D E F -> LeA A B C D E F.
proof: Proof. intros A B C D E F. induction 1. Lea. apply lea_trans with D E F; trivial. apply sams_suma__lea123789 with A B C; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel