Lemma Uint63_canonic :
forall x y,
to_Z x = to_Z y -> x = y.
Lemma ring_theory_switch_eq :
forall A (
R R':
A->A->Prop)
zero one add mul sub opp,
(forall x y :
A,
R x y -> R' x y) ->
ring_theory zero one add mul sub opp R ->
ring_theory zero one add mul sub opp R'.
Lemma Uint63Ring :
ring_theory 0 1
add mul sub opp Logic.eq.
Lemma eq31_correct :
forall x y,
eqb x y = true -> x=y.
Add Ring Uint63Ring :
Uint63Ring
(
decidable eq31_correct,
constants [
Uint63cst]).
Section TestRing.
Let test :
forall x y, 1
+ x*y + x*x + 1
= 1
*1
+ 1
+ y*x + 1
*x*x.
Qed.
End TestRing.
#[
deprecated(
since="8.14",
note="Use isUint63cst instead")]
Ltac isInt63cst :=
isUint63cst.
#[
deprecated(
since="8.14",
note="Use Uint63cst instead")]
Ltac Int63cst :=
Uint63cst.
#[
deprecated(
since="8.14",
note="Use Uint63_canonic instead")]
Notation Int63_canonic :=
Uint63_canonic (
only parsing).
#[
deprecated(
since="8.14",
note="Use Uint63Ring instead")]
Notation Int63Ring :=
Uint63Ring (
only parsing).