proposition: Fact pair_scaleDl u : {morph scale_pair^~ u: a b / a + b}.
proof: Proof. by move=> a b; congr (_, _); apply: scalerDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)