proposition: Lemma pos_set_pos (f : T -> T) e (p p' : positive) : pos (set_pos f e p) p' = if p == p' then f (pos e p) else pos e p'.
proof: Proof. by elim: p e p' => [p IHp|p IHp|] [|???] [?|?|]//=; rewrite IHp. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)