proposition: Lemma ltb_spec: forall m1 n1 m2 n2, is_mask m1 n1 -> is_mask m2 n2 -> (Uint63.ltb m1 m2 = true <-> (n1 < n2)%nat).
proof: Proof. intros. apply mask_spec in H. apply mask_spec in H0. destruct (63 <=? n1)%nat eqn:N1; [tauto|]. destruct (63 <=? n2)%nat eqn:N2; [tauto|]. subst. assert (NS : (n1 <= 62)%nat) by lia. assert (NP : (n2 <= 62)%nat) by lia. rewrite <- Nat.ltb_lt. apply eqb_iff. set (Q:= fun n1 n2=> Bool.eqb (one << int_of_nat n1 <? one << int_of_nat n2)%uint63 (n1 <? n2)%nat). change (Q n1 n2 = true). eapply (forall_2n_correct _ 62 62);auto. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR