The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

lia translates the modulo (you can see when using the preprocessing 
tactic Zify.zify) but seems to lack positivity info about that Z.rem 
function.


On 9/19/21 16:21, Abhishek Anand wrote:
> strange that the following (generalize N.modulo by nf) works:
>
> Require Import NArith.
> Require Import Psatz.
> Axiom nf : N -> N -> N.
> Lemma liatest (n m:N) (p: N.lt N0 m): N.le N0 (nf n m).
>    lia.


--
Laurent