search

esum / internship2019

0 stars 0 forks source link

equiv_eqP #5

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L6 ce lemme peut être évité : si le but est b=b' alors

  apply/eqP/equiv_eqP ; first apply idP ; first apply idP; split.

peut être remplacé par :

  apply/idP/idP.
vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L481 ici on peut remplacer :

  apply/eqP/equiv_eqP.
  apply nthP with (x0:=(0, 0)).
  apply nthP with (x0:=(0, 0)).
  split ; move=> [i H H0] ; apply (mem_nth (0, 0)) in H as H' ;
    rewrite H0 in H' ; rewrite ?prime_decompE in H H0.

par :

apply/(@nthP _ _ _ (0, 0))/(@nthP _ _ _ (0, 0)); move=> [i H H0] ; apply (mem_nth (0, 0)) in H as H' ;
    rewrite H0 in H' ; rewrite ?prime_decompE in H H0.