proposition: Lemma pos_div_eight : forall eps : R, [0] [<] eps -> [0] [<] eps [/]EightNZ.
proof: Proof. intros. apply shift_less_div. apply pos_eight. astepl ([0]:R). assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)