proposition: Lemma divModSucc : forall n p q : nat, fst (Nat.divmod n 1 (S q) p) = S (fst (Nat.divmod n 1 q p)).
proof: Proof. induction n. - intros. reflexivity. - intros. simpl. destruct p. rewrite IHn. reflexivity. rewrite IHn. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase