proposition: Fact test_dual_lt_natdvd (n m : natdvd^d) : (m < n)%O = ~~ (Z.of_nat m =? Z.of_nat n)%Z && (modZ (Z.of_nat m) (Z.of_nat n) =? 0)%Z.
proof: Proof. zify_op; reflexivity. Qed.
imports: Coq(BinInt Zify) mathcomp(all_ssreflect zify ssrZ)