Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import semantics.
Require Import NArith.
Require Import ZArith.
Require Import util.
Import error.
Require List.

Require Import Coq.micromega.Lia.

(*! Logic !*)
Local Notation False := Logic.False.

Lemma negb_is_true:
  forall b : Datatypes.bool, negb b = true <-> ~ is_true b.
Proof.
  intros. destruct b.
  - intuition. elimtype False. apply H. reflexivity.
  - simpl. split; intuition.
Qed.

Lemma bool_false_not b : b = false <-> ~ b.
Proof.
  rewrite (iff_sym (Bool.not_true_iff_false _)).
  destruct b; simpl; split; auto.
Qed.

Lemma bool_reflect_iff :
  forall b1 b2 P Q,
    (b1 = true <-> P) ->
    (b2 = true <-> Q) ->
    (P <-> Q) <-> (b1 = b2).
Proof.
  intros b1 b2 P Q H H0.
  split; intros Hiff; destruct b1, b2; intuition.
Qed.

Lemma some_equal_inv :
  forall A (x y : A),
    Some x = Some y <->
    y = x.
  intuition (f_equal; congruence).
Qed.

Lemma and_both_0_inv { P R S Q } :
  Q <-> S -> P <-> R -> P /\ Q <-> R /\ S.
  intuition.
Qed.

Lemma and_idempotent :
  forall P Q,
    P /\ P /\ Q <-> P /\ Q.
Proof. intuition. Qed.

(* Shim for pair_equal_spec which is not in Coq 8.08 *)
Lemma shim_pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) :
  (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Proof with auto.
  split; intro H.
  - split.
    + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
      rewrite H...
    + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
      rewrite H...
  - destruct H; subst...
Qed.

Lemma iff_both_false :
  forall A B : Prop,
    (A -> False) ->
    (B -> False) ->
    A <-> B.
Proof. intuition. Qed.

(* rename ex_match_error *)
Lemma ex_match :
  forall A (m : M A) P,
    match m with
    | Failed _ _ => False
    | Return x => P x
    end <-> (exists x, m = Return x /\ P x).
Proof.
  intros A m P.
  destruct m.
  - apply iff_both_false; intuition.
    destruct H as [ x [H1 H2] ].
    discriminate.
  - intuition.
    + exists a. intuition.
    + destruct H as [ x [H1 H2] ]. congruence.
Qed.

(* rename ex_match_option *)
Lemma some_match :
  forall A (m : Datatypes.option A) P,
    match m with
    | None => False
    | Some x => P x
    end <-> (exists x, m = Some x /\ P x).
  intros A m P.
  destruct m.
  - intuition.
    + exists a. intuition.
    + destruct H as [ x [H1 H2] ]. congruence.
  - apply iff_both_false; intuition.
    destruct H as [ x [H1 H2] ].
    discriminate.
Qed.

Lemma ex_eq_simpl_some :
  forall (A : Set) (x : A) (P : A -> Prop),
    (exists x' : A, Some x = Some x' /\ P x') <-> P x.
Proof.
  intros A x P.
  transitivity (exists x' : A, x' = x /\ P x').
  apply forall_ex. intro x0. rewrite some_equal_inv. intuition.
  apply ex_eq_simpl.
Qed.

Lemma ex_order3
  : forall (A B C : Type) (P : A -> B -> C -> Prop),
    (exists (x : A) (y : B) (z : C), P x y z) <-> (exists (x : A) (z : C) (y : B), P x y z).
Proof. intros A B C P. split; intros (x, (y, (z, H))); eauto. Qed.

Lemma Is_true_eq_iff :
  forall x : Datatypes.bool,
    x = true <-> Bool.Is_true x.
Proof.
  intros x.
  apply (conj (Bool.Is_true_eq_left x) (Bool.Is_true_eq_true x)).
Qed.

(*! compare !*)

Lemma compare_eq_comm : forall t a b,
    compare t a b = Eq <-> compare t b a = Eq.
Proof.
  intros t a b.
  transitivity (a = b).
  apply compare_eq_iff.
  transitivity (b = a). intuition.
  symmetry. apply compare_eq_iff.
Qed.

Lemma compare_antisym :
  (forall t a b, compare t a b = CompOpp (compare t b a)).
Proof.
  intros t a b.

  destruct (compare t a b) eqn:Hcomp; simpl.
  - apply compare_eq_comm in Hcomp. now rewrite Hcomp.
  - destruct (compare t b a) eqn:Hcomp'; try reflexivity.
    + assert (a <> b). apply compare_diff. intuition.
      apply compare_eq_iff in Hcomp'. congruence.
    + apply compare_gt_lt in Hcomp'. congruence.
  - destruct (compare t b a) eqn:Hcomp'; try reflexivity.
    + assert (a <> b). apply compare_diff. intuition.
      apply compare_eq_iff in Hcomp'. congruence.
    + apply compare_gt_lt in Hcomp'. congruence.
Qed.

Lemma compare_int_compare_spec :
  forall a b, CompareSpec (a = b) (a < b)%Z (b < a)%Z (compare int a b).
Proof. apply Z.compare_spec. Qed.

Lemma compare_nat_compare_spec :
  forall a b, CompareSpec (a = b) (a < b)%N (b < a)%N (compare nat a b).
Proof. apply N.compare_spec. Qed.


Inductive CompareReflection (Peq Plt Pgt : Prop) (c : comparison) : Prop :=
  test : (c = Eq <-> Peq) ->
         (c = Lt <-> Plt) ->
         (c = Gt <-> Pgt) ->
         CompareReflection Peq Plt Pgt c.

Lemma compare_spec_reflection :
  forall (t : comparable_type)
         (a b : comparable_data t)
         (rlt : comparable_data t -> comparable_data t -> Prop),
    (forall {x y}, rlt x y -> rlt y x -> False) ->
    CompSpec eq rlt a b (compare t a b) ->
    CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b).
Proof.
  intros t a b rlt Hirr Hcompspec.
  specialize (Hirr a b).
  split.
  - split.
    + intro Hcompare.
      rewrite Hcompare in Hcompspec.
      now inversion Hcompspec.
    + now rewrite compare_eq_iff.
  - split.
    + intro Hcompare.
      rewrite Hcompare in Hcompspec.
      now inversion Hcompspec.
    + intro Hineq.
      destruct (compare t a b) eqn:Hcomp; inversion Hcompspec; subst; intuition.
  - split.
    + intro Hcompare.
      rewrite Hcompare in Hcompspec.
      now inversion Hcompspec.
    + intro Hineq.
      destruct (compare t a b) eqn:Hcomp; inversion Hcompspec; subst; intuition.
Qed.

Definition compare_reflection_nat (n1 n2 : N) :
  CompareReflection (n1 = n2) (n1 < n2)%N (n2 < n1)%N (compare nat n1 n2)
  := compare_spec_reflection nat n1 n2 N.lt N.lt_asymm (N.compare_spec n1 n2).

Definition compare_reflection_int (n1 n2 : Z) :
  CompareReflection (n1 = n2) (n1 < n2)%Z (n2 < n1)%Z (compare int n1 n2)
  := compare_spec_reflection int n1 n2 Z.lt Z.lt_asymm (Z.compare_spec n1 n2).

Definition mutez_compare_spec :
  forall (n1 n2 : tez.mutez),
    CompareSpec (n1 = n2)
                (tez.to_Z n1 < tez.to_Z n2)%Z
                (tez.to_Z n2 < tez.to_Z n1)%Z
                (compare mutez n1 n2).
Proof.
  intros n1 n2.
  assert
    (CompareSpec (tez.to_Z n1 = tez.to_Z n2)
                 (tez.to_Z n1 < tez.to_Z n2)%Z
                 (tez.to_Z n2 < tez.to_Z n1)%Z
                 (compare mutez n1 n2))
    by apply Z.compare_spec.
  destruct (compare mutez n1 n2); inversion H; constructor; try assumption.
  now apply tez.to_Z_inj.
Qed.

Definition compare_reflection_mutez (n1 n2 : tez.mutez) :
  CompareReflection (n1 = n2)
                    (tez.to_Z n1 < tez.to_Z n2)%Z
                    (tez.to_Z n2 < tez.to_Z n1)%Z
                    (compare mutez n1 n2).
Proof.
  apply (compare_spec_reflection mutez
                                 n1
                                 n2
                                 (fun n1 n2 => (tez.to_Z n1 < tez.to_Z n2)%Z)).
  - intros x y.
    apply Z.lt_asymm.
  - apply mutez_compare_spec.
Qed.

Lemma compare_nat_lt : forall (n1 n2 : N), compare nat n1 n2 = Lt <-> (n1 < n2)%N.
Proof. intros n1 n2.
       pose proof (N.compare_spec n1 n2).
       inversion H; intuition. Qed.
Lemma compare_nat_gt : forall (n1 n2 : N), compare nat n1 n2 = Gt <-> (n1 > n2)%N.
Proof. intros n1 n2.
       pose proof (N.compare_spec n1 n2).
       inversion H; intuition. Qed.
Lemma compare_int_lt : forall (n1 n2 : Z), compare int n1 n2 = Lt <-> (n1 < n2)%Z.
Proof. intros n1 n2.
       pose proof (Z.compare_spec n1 n2).
       inversion H; intuition. Qed.
Lemma compare_int_gt : forall (n1 n2 : Z), compare int n1 n2 = Gt <-> (n1 > n2)%Z.
Proof. intros n1 n2.
       pose proof (Z.compare_spec n1 n2).
       inversion H; intuition. Qed.
Lemma compare_mutez_lt : forall (n1 n2 : tez.mutez), compare mutez n1 n2 = Lt <-> (tez.to_Z n1 < tez.to_Z n2)%Z.
Proof. intros n1 n2.
       pose proof (mutez_compare_spec n1 n2).
       inversion H; intuition.
Qed.
Lemma compare_mutez_gt : forall (n1 n2 : tez.mutez), compare mutez n1 n2 = Gt <-> (tez.to_Z n1 > tez.to_Z n2)%Z.
Proof.
  intros n1 n2.
  pose proof (mutez_compare_spec n1 n2).
  inversion H; intuition.
Qed.

(*! comparison_to_int !*)

Lemma comp_to_int_Eq c : (comparison_to_int c =? 0)%Z = true <-> c = Eq.
Proof.
  destruct c; simpl; split; auto; discriminate.
Qed.

Lemma comp_to_int_Lt c : (comparison_to_int c <? 0)%Z = true <-> c = Lt.
Proof.
  destruct c; simpl; split; auto; discriminate.
Qed.

Lemma comp_to_int_Gt c : (comparison_to_int c >? 0)%Z = true <-> c = Gt.
Proof.
  destruct c; simpl; split; auto; discriminate.
Qed.

Lemma comparison_to_int_N_compare_le x y : (comparison_to_int (x ?= y)%N >=? 0)%Z = true <-> (x >= y)%N.
Proof.
  unfold N.ge; destruct (x ?= y)%N; simpl; unfold Z.geb; simpl; split; auto.
  2: discriminate.
  all: intros _ H; discriminate.
Qed.

Lemma comparison_to_int_Z_compare_ltb:
  forall z1 z2 : Z, (comparison_to_int (z1 ?= z2) <? 0)%Z = (z1 <? z2)%Z.
Proof.
  intros z1 z2.

  destruct (Z.compare_spec z1 z2); simpl.
  - rewrite H.
    now repeat rewrite Z.ltb_irrefl.
  - apply Z.ltb_lt in H.
    rewrite H.
    reflexivity.
  - apply Z.lt_asymm in H.
    apply Z.ltb_nlt in H.
    rewrite H.
    reflexivity.
Qed.

Lemma comparison_to_int_pos :
  forall n,
    (comparison_to_int
       match n with
       | 0%N => Eq
       | N.pos _ => Lt
       end <? 0)%Z = true <-> (n > 0)%N.
Proof.
  intro n. destruct n. simpl. cbv. intuition congruence.
  simpl. intuition. lia.
Qed.

Lemma comparison_to_int_N_opp:
  forall (n1 n2 : N),
    (comparison_to_int (n2 ?= n1)%N >=? 0)%Z =
    (comparison_to_int (n1 ?= n2)%N <=? 0)%Z.
Proof.
  intros n1 n2.
  rewrite N.compare_antisym.
  destruct (n1 ?= n2)%N; simpl; tauto.
Qed.

(*! comparison_to_int compare !*)

Lemma comparison_to_int_compare_gt_lt:
  forall (t : comparable_type) (a b : comparable_data t),
    (comparison_to_int (compare t a b) <? 0)%Z = true <->
    (comparison_to_int (compare t b a) >? 0)%Z = true.
Proof.
  intros t a b.
  rewrite comp_to_int_Lt, comp_to_int_Gt.
  apply compare_gt_lt.
Qed.

Lemma comparison_to_int_compare_gt_lt_eq:
  forall (t : comparable_type) (a b : comparable_data t),
    (comparison_to_int (compare t a b) <? 0)%Z =
    (comparison_to_int (compare t b a) >? 0)%Z.
Proof.
  intros t a b.
  apply Bool.eq_true_iff_eq.
  apply (comparison_to_int_compare_gt_lt t a b).
Qed.

Lemma comparison_to_int_compare_lt :
  forall (t : comparable_type)
         (a b : comparable_data t)
         (rlt : comparable_data t -> comparable_data t -> Prop),
    CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b) ->
    (comparison_to_int (compare t a b) <? 0)%Z = true <-> (rlt a b)%Z.
Proof.
  intros t a b rlt H.
  rewrite comp_to_int_Lt.
  apply H.
Qed.

Lemma comparison_to_int_compare_gt :
  forall (t : comparable_type)
         (a b : comparable_data t)
         (rlt : comparable_data t -> comparable_data t -> Prop),
    CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b) ->
    (comparison_to_int (compare t a b) >? 0)%Z = true <-> (rlt b a)%Z.
Proof.
  intros t a b rlt H.
  rewrite comp_to_int_Gt.
  apply H.
Qed.

Lemma comparison_to_int_compare_ge :
  forall (t : comparable_type)
         (a b : comparable_data t),
    (comparison_to_int (compare t a b) >=? 0)%Z = true <-> (compare t a b) <> Lt.
Proof.
  intros t a b. destruct (compare t a b); simpl; cbv; intuition discriminate.
Qed.

Lemma comparison_to_int_compare_le :
  forall (t : comparable_type)
         (a b : comparable_data t),
    (comparison_to_int (compare t a b) <=? 0)%Z = true <-> (compare t a b) <> Gt.
Proof.
  intros t a b. destruct (compare t a b); simpl; cbv; intuition discriminate.
Qed.

Lemma comparison_to_int_compare_int_lt :
  forall (z1 z2 : Z),
    (comparison_to_int (compare int z1 z2) <? 0)%Z = true <-> (z1 < z2)%Z.
Proof. intros z1 z2.
       apply (comparison_to_int_compare_lt int _ _ _ (compare_reflection_int _ _)).
Qed.

Lemma comparison_to_int_compare_int_gt :
  forall (z1 z2 : Z),
    (comparison_to_int (compare int z1 z2) >? 0)%Z = true <-> (z1 > z2)%Z.
Proof. intros z1 z2.
       rewrite Z.gt_lt_iff.
       apply (comparison_to_int_compare_gt int _ _ _ (compare_reflection_int _ _)).
Qed.

Lemma comparison_to_int_compare_int_ge :
  forall (z1 z2 : Z),
    (comparison_to_int (compare int z1 z2) >=? 0)%Z = true <-> (z1 >= z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge int z1 z2). Qed.

Lemma comparison_to_int_compare_int_le :
  forall (z1 z2 : Z),
    (comparison_to_int (compare int z1 z2) <=? 0)%Z = true <-> (z1 <= z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_le int z1 z2). Qed.


Lemma comparison_to_int_compare_nat_lt :
  forall (z1 z2 : N),
    (comparison_to_int (compare nat z1 z2) <? 0)%Z = true <-> (z1 < z2)%N.
Proof. intros z1 z2.
       apply (comparison_to_int_compare_lt nat _ _ _ (compare_reflection_nat _ _)).
Qed.

Lemma comparison_to_int_compare_nat_gt :
  forall (z1 z2 : N),
    (comparison_to_int (compare nat z1 z2) >? 0)%Z = true <-> (z1 > z2)%N.
Proof. intros z1 z2.
       rewrite N.gt_lt_iff.
       apply (comparison_to_int_compare_gt nat _ _ _ (compare_reflection_nat _ _)).
Qed.

Lemma comparison_to_int_compare_nat_ge :
  forall (z1 z2 : N),
    (comparison_to_int (compare nat z1 z2) >=? 0)%Z = true <-> (z1 >= z2)%N.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge nat z1 z2). Qed.

Lemma comparison_to_int_compare_nat_le :
  forall (z1 z2 : N),
    (comparison_to_int (compare nat z1 z2) <=? 0)%Z = true <-> (z1 <= z2)%N.
Proof. intros z1 z2. apply (comparison_to_int_compare_le nat z1 z2). Qed.

Lemma comparison_to_int_compare_nat_eqb :
  forall n1 n2,
    (comparison_to_int (compare nat n1 n2) =? 0)%Z = N.eqb n1 n2.
Proof.
  intros n1 n2.
  apply Bool.eq_iff_eq_true.
  rewrite N.eqb_eq.
  apply eqb_eq.
Qed.

Definition mutez_lt n1 n2 := (tez.to_Z n1 < tez.to_Z n2)%Z.

Lemma comparison_to_int_compare_mutez_lt :
  forall (z1 z2 : tez.mutez),
    (comparison_to_int (compare mutez z1 z2) <? 0)%Z = true <-> (tez.to_Z z1 < tez.to_Z z2)%Z.
Proof. intros z1 z2.
       apply (comparison_to_int_compare_lt mutez z1 z2 mutez_lt (compare_reflection_mutez _ _)).
Qed.

Lemma comparison_to_int_compare_mutez_gt :
  forall (z1 z2 : tez.mutez),
    (comparison_to_int (compare mutez z1 z2) >? 0)%Z = true <-> (tez.to_Z z1 > tez.to_Z z2)%Z.
Proof. intros z1 z2.
       rewrite Z.gt_lt_iff.
       apply (comparison_to_int_compare_gt mutez z1 z2 mutez_lt (compare_reflection_mutez _ _)).
Qed.

Lemma comparison_to_int_compare_mutez_ge :
  forall (z1 z2 : tez.mutez),
    (comparison_to_int (compare mutez z1 z2) >=? 0)%Z = true <-> (tez.to_Z z1 >= tez.to_Z z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge mutez z1 z2). Qed.

Lemma comparison_to_int_compare_mutez_le :
  forall (z1 z2 : tez.mutez),
    (comparison_to_int (compare mutez z1 z2) <=? 0)%Z = true <-> (tez.to_Z z1 <= tez.to_Z z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_le mutez z1 z2). Qed.

Lemma comparison_to_int_compare_int_geb :
  forall (z1 z2 : Z),
    (comparison_to_int (compare int z1 z2) >=? 0)%Z = (z1 >=? z2)%Z.
Proof.
  intros z1 z2.
  apply (bool_reflect_iff _ _ (z1 >= z2)%Z (z1 >= z2)%Z).
  apply comparison_to_int_compare_int_ge.
  rewrite Z.geb_le.
  rewrite Z.ge_le_iff.
  reflexivity.
  reflexivity.
Qed.

Lemma comparison_to_int_eq_comm : forall t a b,
    (comparison_to_int (compare t a b) =? 0)%Z =
    (comparison_to_int (compare t b a) =? 0)%Z.
Proof.
  intros t a b.
  rewrite compare_antisym.
  destruct (compare t b a); reflexivity.
Qed.

(* todo: change tez.compare to compare? *)
Lemma tez_to_Z_bij :
  forall t1 t2 : tez.mutez, tez.to_Z t1 = tez.to_Z t2 <-> t1 = t2.
Proof.
  split. apply tez.to_Z_inj. intro. now f_equal.
Qed.

Lemma Tez2N_inj_iff :
  forall t1 t2,
    (Z.to_N (tez.to_Z t1) = Z.to_N (tez.to_Z t2) <-> t1 = t2).
  intros t1 t2.
  rewrite Z2N.inj_iff; [|apply tez.to_Z_lower_bound|apply tez.to_Z_lower_bound].
  now rewrite tez_to_Z_bij.
Qed.
  
Lemma tez_to_Z_to_N_neq_zero_iff :
  forall t : tez.mutez,
    Z.to_N (tez.to_Z t) <> 0%N <-> t <> (0 ~Mutez).
Proof.
  intros t.
  change 0%N with (Z.to_N (tez.to_Z (0 ~Mutez))).
  now rewrite Tez2N_inj_iff.
Qed.

Lemma comparison_to_int_tez_compare_le_zero:
  forall t,
    (comparison_to_int (compare mutez t (0 ~Mutez)) <=? 0)%Z = true <->
    (t = (0 ~Mutez)).
Proof.
  intros t.
  rewrite comparison_to_int_compare_mutez_le.
  rewrite <- tez_to_Z_bij.
  pose proof (tez.to_Z_lower_bound t) as Hlb.
  change 0%Z with (tez.to_Z (0 ~Mutez)) in Hlb.
  lia.
Qed.

Lemma comparison_to_int_tez_compare_lt_zero:
  forall t,
    (comparison_to_int (compare mutez (0 ~Mutez) t) <? 0)%Z = true <->
    (t <> (0 ~Mutez)).
Proof.
  intros t.
  change tez.compare with (compare mutez).
  rewrite <- Bool.not_false_iff_true.
  apply not_iff_compat.
  rewrite <- comparison_to_int_tez_compare_le_zero.
  change tez.compare with (compare mutez).
  rewrite <- Bool.negb_false_iff.
  rewrite <- lt_is_leb.

  rewrite comparison_to_int_compare_gt_lt_eq.

  reflexivity.
Qed.

Lemma comparison_to_int_tez_compare_mutez_to_nat :
  forall t1 t2,
    (comparison_to_int (compare mutez t1 t2) <=? 0)%Z = true <->
    ((Z.to_N (tez.to_Z t1)) <= (Z.to_N (tez.to_Z t2)))%N.
Proof.
  intros t t'.
  rewrite comparison_to_int_compare_mutez_le.
  rewrite Z2N.inj_le; try apply tez.to_Z_lower_bound.
  reflexivity.
Qed.

(*! ediv_N !*)

Lemma ediv_spec a b d r :
  ediv_N a b = Some (d, r) <-> (d = (a / b)%N /\ r = (a mod b)%N) /\ (0 < b)%N.
Proof.
  unfold ediv_N; destruct b; simpl; split.
  - discriminate.
  - lia.
  - intro H; injection H; intros Hr Hd; rewrite Hr, Hd; unfold N.lt; simpl; auto.
  - intros [[Hd Hr] _]; rewrite Hd, Hr; auto.
Qed.

Lemma ediv_N_some_iff :
  forall (x y : N) Q,
    y <> 0%N /\ Q ((x / y)%N, (x mod y)%N) <->
    (exists z, ediv_N x y = Some z /\ Q z).
Proof.
  intros.
  split.
  - intros [H1 H2].
    exists ((x / y)%N, (x mod y)%N).
    split.
    apply ediv_spec. intuition lia.
    assumption.
  - unfold ediv_N.
    intros [z [Hdiv Hq]].
    rewrite <- N.eqb_eq. rewrite <- bool_not_false.
    destruct (y =? 0)%N.
    + discriminate.
    + intuition congruence.
Qed.

Lemma Z_mod_to_N_mod :
  forall x y, (Z.of_N (x mod y) =? 0)%Z = true <-> (x mod y)%N = 0%N.
  intros x y.
  destruct (_ =? _)%Z eqn:Heq.
  rewrite Z.eqb_eq in Heq.
  rewrite <- N2Z.inj_iff.
  now intuition.
  intuition. inversion H.
  rewrite <- Heq. rewrite H. reflexivity.
Qed.

(*! About tez !*)

Lemma mutez_to_nat :
  forall t,
    match tez.of_Z (Z.of_N (Z.to_N (tez.to_Z t mod tez.to_Z (1 ~Mutez)))) with
    | Failed _ _ => None
    | Return rem => Some (Z.to_N (tez.to_Z t / tez.to_Z (1 ~Mutez)), rem)
    end = Some (Z.to_N (tez.to_Z t), (0 ~Mutez)).
Proof. intro t. now rewrite Z.mod_1_r, Z.div_1_r. Qed.

Lemma tez_neq_zero_iff_gt_zero t :
  t <> (0 ~Mutez) <-> (0 < Z.to_N (tez.to_Z t))%N.
Proof.
  change 0%N with (Z.to_N (tez.to_Z (0 ~Mutez))).
  rewrite <- tez_to_Z_bij.
  rewrite <- Z2N.inj_iff by apply tez.to_Z_lower_bound.
  split; simpl; intro H; lia.
Qed.

(*! About N !*)

Lemma nat_neq_zero_iff_gt_zero:
  forall m : N,
    (m <> 0 <-> 0 < m)%N.
Proof.
  (* solved directly by lia in later versions of coq. *)
  destruct m; lia.
Qed.

(*! About Z !*)

Lemma match_z_eq :
  forall (z : Z),
    (match z with
     | 0 => 0
     | Z.pos y' => Z.pos y'
     | Z.neg y' => Z.neg y'
     end)%Z = z.
Proof. destruct z; reflexivity. Qed.

Lemma Z_abs_N_sub :
  forall (n1 n2 : N),
    (0 <= Z.of_N n1 - Z.of_N n2)%Z ->
    Z.abs_N (Z.of_N n1 - Z.of_N n2)%Z =
    (n1 - n2)%N.
Proof.
  intros n1 n2 H.
  rewrite Zabs2N.inj_sub.
  now do 2 rewrite Zabs2N.id.
  lia.
Qed.

Lemma Z_gtb_false_leb_iff :
  forall x y,
    (x >? y = false <-> x <=? y = true)%Z.
Proof.
  intros x y. rewrite Z.gtb_ltb, Z.ltb_nlt, Z.leb_le. lia.
Qed.

Lemma Z_ltb_false_geb_iff :
  forall x y,
    (x <? y = false <-> x >=? y = true)%Z.
Proof.
  intros x y. rewrite Z.ltb_nlt, Z.geb_le. lia.
Qed.

(** todo *)

Lemma cmp_nat_lt_zero n :
  (comparison_to_int (compare nat 0 n)%N <? 0)%Z = true <->
  (n <> 0)%N.
Proof.
  rewrite comparison_to_int_compare_nat_lt.
  symmetry.
  apply nat_neq_zero_iff_gt_zero.
Qed.

(** TODO: could just use comparison_to_int_compare_gt_lt instead *)
Lemma cmp_mutez_gt_lt t :
  (comparison_to_int (compare mutez t (0 ~Mutez)) >? 0)%Z = true <->
  (comparison_to_int (compare mutez (0 ~Mutez) t) <? 0)%Z = true.
Proof.
  change tez.compare with (compare mutez). symmetry.
  apply comparison_to_int_compare_gt_lt.
Qed.

Lemma tez_fact_l:
  forall (min_x : tez.mutez)
         (x' : N)
         (x : tez.mutez),
    tez.to_Z x = Z.of_N x' ->
    (Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N ->
    (x' >= Z.to_N (tez.to_Z min_x))%N.
Proof.
  intros min_x x' x H.
  intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.

Lemma tez_fact_r:
  forall (min_x : tez.mutez)
         (x' : N)
         (x : tez.mutez),
    tez.to_Z x = Z.of_N x' ->
    (x' >= Z.to_N (tez.to_Z min_x))%N ->
    (Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N.
Proof.
  intros min_x x' x H.
  intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.


(* Not sure where to put this *)
Definition get_amount_bought_rem x y z
  := ((x * 997 * z) mod (y * 1000 + x * 997))%N.