proposition: Lemma div_spec : forall n m q r, n >= 0 -> m > 0 -> (q,r) = div n m -> n = q*m + r /\ r < m.
proof: Proof. Proof using. intros n. induction_wf IH: (downto 0) n. introv Hn Hm Eq. rewrite* fix_div in Eq. unfolds Div. case_if. { inverts* Eq. } { gen Eq. case_eq (div (n-m) m) ;=> q' r' E Eq. inverts Eq. symmetry in E. forwards* (Hq',Hr'): IH E. { hnfs*. } } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat