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