proposition: Theorem pred_lt_le : forall x y, (x <> 0)%R -> (x <= y)%R -> (pred x < y)%R.
proof: Proof. intros x y Zy Hxy. apply Rlt_le_trans with (2 := Hxy). now apply pred_lt_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop