search

esum / internship2019

0 stars 0 forks source link

pose proof _ as _ #16

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L413-L414 en ssreflect on écrit plutôt :

  move: (coprime_dvdr p_coprime_n m_coprime_n)=> m_coprime_p.
  move: (coprime_dvdl p_coprime_m m_coprime_p)=> p_coprime_p.

ou encore simplement :

  move: (coprime_dvdr p_coprime_n m_coprime_n).
  move: (coprime_dvdl p_coprime_m m_coprime_p).

pour garder les assertions dans le but (c.f. issue #11)