proposition: Lemma fix_div : forall n m, n >= 0 /\ m > 0 -> div n m = Div div n m.
proof: Proof. Proof using. applys~ (FixFun2_fix_partial (unproj21 Z (downto 0))). introv (Hn&Hm) IH. unfold Div. case_if~. rewrite* IH. { hnf. math. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat