proposition: Lemma remainder_terminates: forall a b, b > 0 -> exists q r, terminates (remainder a b) r /\ r < b /\ a = b * q + r.
proof: Proof. induction a using (well_founded_ind lt_wf). intros. unroll_delay (remainder a b). destruct (Nat.ltb_spec a b). - exists 0, a. split. constructor. split. auto. lia. - assert (LT: a - b < a) by lia. destruct (H _ LT b H0) as (q & r & P & Q & R). exists (S q), r. split. constructor; auto. split. auto. lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)