nat_mod_lt_r' n m r : r < m -> n mod m < m. Proof. intros H; destruct H; only 1: exact _. rapply (lt_leq_lt_trans (m:=m)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes