proposition: Lemma fix_div : forall n m, m <> 0 -> div n m = Div div n m.
proof: Proof. Proof using. applys~ (FixFun2_fix_partial (measure (@fst nat nat))). introv Posm IH. unfold Div. case_if~. rewrite~ IH. unfolds. simpl. math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat