Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L192 destruct n'est pas utilisé en ssreflect. L'équivalent de la ligne ci-dessus est :
destruct
case n_decomp: (prime_decomp n)=> [|[p a] t] ; first by rewrite /primepow n_decomp.
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L192
destruct
n'est pas utilisé en ssreflect. L'équivalent de la ligne ci-dessus est :