anti_ltn

[vblot]

internship2019/src/arith.v

Line 16 in 17e55db

Lemma anti_ltn : antisymmetric ltn.

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.