proposition: Lemma qsum_exten f g n: natp n -> same_below f g n -> qsum f n = qsum g n.
proof: Proof. move:n;apply: Nat_induction; first by move => _; rewrite !qsum0. move => n nN Hrec h1; rewrite (qsum_rec f nN) (qsum_rec g nN). congr (_ +q _). by apply: h1; apply: cltS. by apply: Hrec => i [/(cltSleP nN) /h1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)