proposition: Lemma grada_out__out : forall A B C D E F, Out E D F -> GradA A B C D E F -> Out B A C.
proof: Proof. intros A B C D E F Hout HGA. apply out_lea__out with D E F; trivial. apply grada__lea; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel