proposition: Lemma Z_of_N_ZtoN : forall n, (0 <= n)%Z -> Z_of_N (ZtoN n) = n.
proof: Proof. intros [|p|p] H ; [easy|easy|]. now elim H. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux