I think there should be spec lemma for `bigO` to avoid these patterns: `have /bigOFP [_/posnumP[c1] kOg] := bigOP [bigO of k]`
I think there should be spec lemma for
bigOto avoid these patterns:have /bigOFP [_/posnumP[c1] kOg] := bigOP [bigO of k]