Commit 53df9d8b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Renamed theorems.

parent 5f48113c
......@@ -261,7 +261,7 @@ rewrite (Zle_antisym _ _ Hx' Hx).
apply digits_ge_0.
Qed.
Theorem digits_lt :
Theorem lt_digits :
forall x y,
(0 <= y)%Z ->
(digits x < digits y)%Z ->
......
......@@ -113,7 +113,7 @@ assert (Hq': (0 < q)%Z).
apply Zmult_lt_reg_r with m2.
exact Hm2'.
assert (m2 < m')%Z.
apply digits_lt with beta.
apply lt_digits with beta.
now apply Zlt_le_weak.
unfold d2 in Hs3.
omega.
......@@ -150,4 +150,4 @@ apply bpow_gt_0.
now apply (Z2R_lt 0).
Qed.
End Fcalc_div.
\ No newline at end of file
End Fcalc_div.
......@@ -1516,7 +1516,7 @@ apply -> bpow_lt.
now apply Zgt_lt.
Qed.
Theorem bpow_eq :
Theorem bpow_inj :
forall e1 e2 : Z,
bpow e1 = bpow e2 -> e1 = e2.
Proof.
......
......@@ -967,7 +967,7 @@ case Req_bool_spec; intros Hy2.
(* . *)
intros Hy3.
assert (ey-1 = fexp (ey -1))%Z.
apply bpow_eq with beta.
apply bpow_inj with beta.
rewrite <- Hy2, <- Rplus_0_l, Hy3.
ring.
assert (Zx: (x <> 0)%R).
......
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