proposition: Lemma scanlK : (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).
proof: Proof. by move=> Hfg x s; elim: s x => //= y s IHs x; rewrite Hfg IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)