proposition: Theorem pred_lt_id : forall x, (x <> 0)%R -> (pred x < x)%R.
proof: Proof. intros x Zx; unfold pred. pattern x at 2; rewrite <- (Ropp_involutive x). apply Ropp_lt_contravar. apply succ_gt_id. auto with real. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop