search

esum / internship2019

0 stars 0 forks source link

nth #15

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L310-L324 ici et à plusieurs autres endroits tu passes par nth, ce qui n'est pas nécessaire. Par exemple le morceau de preuve ci-dessus peut être remplacé par :

    move=> n_p_dvd_m b.
    rewrite eqnE eq_sym.
    move/mapP=> [n].
    rewrite mem_index_iota=> /andP [] n_gt_0 _ ->.
    rewrite eqb0.
    apply/negP=> n_p_n_dvd_m.
    apply: n_p_dvd_m.
    by apply (dvdn_exp2 _ _ n).