search

esum / internship2019

0 stars 0 forks source link

ltn_0_prod #8

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L59 ce lemme n'est pas utilisé (et se prouve trivialement à partir de ltn_0_prod_f et map_id)