proposition: Theorem Rlt_Float_Zlt : forall p q r : Z, (Float p r < Float q r)%R -> (p < q)%Z.
proof: Proof. intros p q r H'. apply lt_IZR. apply Rlt_monotony_contra_exp with (z := r); auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz