nth

[vblot]

internship2019/src/arith.v

Lines 310 to 324 in 17e55db

	move=> n_p_dvd_m b b_in.
	rewrite eqnE eq_sym.
	move/nthP in b_in.
	destruct (b_in 0) as [i H H0].
	rewrite size_map in H.
	rewrite (nth_map 1) // in H0.
	rewrite -H0 eqn0_negb.
	apply/negP.
	move=> H1.
	apply n_p_dvd_m.
	apply dvdn_exp2 with (nth 1 (index_iota 1 m) i) ; last by [].
	assert (nth 1 (index_iota 1 m) i \in (index_iota 1 m)) as e_in_iota ; first by apply mem_nth.
	rewrite mem_index_iota in e_in_iota.
	move/andP in e_in_iota.
	by destruct e_in_iota.

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).