proposition: Lemma qltone : forall q : R, q [<] [1] -> q[-][1] [#] [0].
proof: Proof. intros. apply less_imp_ap. apply shift_minus_less. astepr ([1]:R). auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)