fact: Record axioms R : Prop := Axioms { le_reflexive (x : val R) : le x x; le_transitive (x y z : val R) : le x y -> le y z -> le x z; sup_upper_bound (E : set R) : has_sup E -> ub E (sup E); sup_total (E : set R) (x : val R) : has_sup E -> down E x \/ le (sup E) x; add_monotone (x y z : val R) : le y z -> le (add x y) (add x z); add_commutative (x y : val R) : eq (add x y) (add y x); add_associative (x y z : val R) : eq (add x (add y z)) (add (add x y) z); add_zero_left (x : val R) : eq (add (zero R) x) x; add_opposite_right (x : val R) : eq (add x (opp x)) (zero R); mul_monotone x y z : le (zero R) x -> le y z -> le (mul x y) (mul x z); mul_commutative (x y : val R) : eq (mul x y) (mul y x); mul_associative (x y z : val R) : eq (mul x (mul y z)) (mul (mul x y) z); mul_distributive_right (x y z : val R) : eq (mul x (add y z)) (add (mul x y) (mul x z)); mul_one_left (x : val R) : eq (mul (one R) x) x; mul_inverse_right (x : val R) : ~ eq x (zero R) -> eq (mul x (inv x)) (one R); one_nonzero : ~ eq (one R) (zero R) }.