factorisation de preuves

[vblot]

internship2019/src/arith.v

Lines 377 to 392 in 17e55db

	destruct (coprime p m)eqn:p_coprime_m.
	apply/orP.
	left.
	apply/allP.
	move=> b b_in.
	move/nthP in b_in.
	destruct (b_in false) as [i Hb Hb0].
	rewrite size_map in Hb.
	rewrite (nth_map (0, 0) false) // in Hb0.
	remember (nth (0, 0) (prime_decomp m) i) as q ; destruct q as [q a].
	rewrite -Hb0 eq_sym bool_eq_true.
	apply coprime_dvdr with m ; last by [].
	apply (mem_nth (0, 0)) in Hb.
	rewrite -Heqq in Hb.
	apply mem_prime_decomp in Hb.
	apply dvdn_exp2 with a ; by destruct Hb.

ce morceau de preuve est répété deux fois d'affilée. Il serait mieux de prouver par exemple le lemme :

forall p m, coprime p m -> all (coprime p) (primes m).

[vblot]

idem ici :

internship2019/src/arith.v

Lines 416 to 441 in 17e55db

	apply/allP ; move=> f f_in.
	move/nthP in f_in.
	pose proof (f_in 0) as [i Hi Hf].
	rewrite size_map in Hi.
	rewrite (nth_map (0, 0)) // in Hf.
	remember (nth (0, 0) (prime_decomp n) i) as q ; destruct q as [q a].
	rewrite -Hf /=.
	rewrite expn_gt0.
	apply (mem_nth (0, 0)) in Hi.
	rewrite -Heqq in Hi.
	apply mem_prime_decomp in Hi.
	destruct Hi as [q_prime _ _].
	rewrite prime_gt0 //.
	apply/allP ; move=> f f_in.
	move/nthP in f_in.
	pose proof (f_in 0) as [i Hi Hf].
	rewrite size_map in Hi.
	rewrite (nth_map (0, 0)) // in Hf.
	remember (nth (0, 0) (prime_decomp m) i) as q ; destruct q as [q a].
	rewrite -Hf /=.
	rewrite expn_gt0.
	apply (mem_nth (0, 0)) in Hi.
	rewrite -Heqq in Hi.
	apply mem_prime_decomp in Hi.
	destruct Hi as [q_prime _ _].
	rewrite prime_gt0 //.

[vblot]

J'en ai encore repéré plusieurs à d'autres endroits, il faudrait reprendre tes preuves et essayer de factoriser partout où il y a du copier-coller.