proposition: Lemma helper1 n1 n2 n3 : (n2 > 0)%N -> (n3 > 0)%N -> ((n1 %/ n2) %/ n3)%N = floorQ (n1%:Q / (n2 * n3)%N%:Q) :> int.
proof: Proof. case: n2 =>[|n2] //; case: n3 => [|n3] // => Hpos2 Hpos3. by rewrite -divnMA mulSn addSn floorQ_divn -floorQ_int. Qed.
imports: mathcomp(all_ssreflect all_algebra)