Open affeldt-aist opened 1 year ago
https://github.com/affeldt-aist/trajectories/blob/1be5acf4fcbeaabe96a52c1ae491f24bfea81f3a/theories/conv.v#L129
shouldn't this be eqVneq ((1 - t) * (1 - u)) 1. instead to limit the use of subr_eq0
eqVneq ((1 - t) * (1 - u)) 1.
https://github.com/affeldt-aist/trajectories/blob/1be5acf4fcbeaabe96a52c1ae491f24bfea81f3a/theories/conv.v#L129
shouldn't this be
eqVneq ((1 - t) * (1 - u)) 1.instead to limit the use of subr_eq0