proposition: Lemma lesb_ltb : forall x, lesb 0 x = Uint63.ltb x min_int.
proof: Proof. intros x. destruct (Uint63.ltb x min_int) eqn:H; destruct (lesb 0 x) eqn:H'; [easy | | | easy]. { destruct (lebP 0 x) as [_ | P]; [easy |]. clear H'. change (to_Z 0) with 0%Z in P. unfold to_Z in P. rewrite H in P. generalize (Uint63.to_Z_bounded x); lia. } destruct (lebP 0 x) as [P | _]; [| easy]. clear H'. change (to_Z 0) with 0%Z in P. unfold to_Z in P. rewrite H in P. destruct (Uint63.ltbP x min_int) as [_ | P']; [easy |]. clear H. destruct (Uint63.eqb (- x) 0) eqn:H. { apply eqb_correct in H. change 0%uint63 with (- 0)%uint63 in H. apply PrimInt63_opp_inj in H. rewrite H in P'. cbn in P'. lia. } destruct (eqbP (- x) 0) as [_ | P'']; [easy |]. assert (H': x <> 0%uint63) by now intros ->. apply Zle_lt_or_eq in P. destruct P as [P | P]; [generalize (Uint63.to_Z_bounded (- x)); lia |]. change 0%Z with (- 0)%Z in P. apply Z.opp_inj in P. change 0%Z with (Uint63.to_Z 0) in P. apply Uint63.to_Z_inj in P. now rewrite <- P in P''. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)