Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L16 Même si c'est formellement vrai, c'est très troublant de lire que < est antisymmétrique. Il me semble que tu utilises ce lemme uniquement avec sorted_primes. Il serait plus naturel de montrer :
sorted_primes_leq : forall n : nat, sorted (T:=nat_eqType) leq (primes n)
ou encore :
sorted_leq_ltn : forall s, sorted ltn s -> sorted leq s
qui se prouve facilement avec ltn_sorted_uniq_leq.
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L16 Même si c'est formellement vrai, c'est très troublant de lire que < est antisymmétrique. Il me semble que tu utilises ce lemme uniquement avec sorted_primes. Il serait plus naturel de montrer :
ou encore :
qui se prouve facilement avec ltn_sorted_uniq_leq.