Commit 7efae3f8 authored by MARCHE Claude's avatar MARCHE Claude

more lemmas on div real

parent a1e3ab18
......@@ -89,6 +89,19 @@ theory Field
function inv t : t
axiom Inverse : forall x:t. x <> zero -> x * inv x = one
function (/) (x y : t) : t = x * inv y
lemma assoc_mul_div: forall x y z:real.
(* todo: discard the hypothesis ? *)
z <> zero -> (x*y)/z = x*(y/z)
lemma assoc_div_mul: forall x y z:real.
(* todo: discard the hypothesis ? *)
y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)
lemma assoc_div_div: forall x y z:real.
(* todo: discard the hypothesis ? *)
y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y
end
theory OrderedField
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment