RealInfix.v 166 Bytes
Newer Older
1 2 3 4 5 6 7
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Require real.Real.