proposition: Theorem lt_wf_0 : well_founded lt.
proof: Proof. setoid_replace lt with (fun n m => 0 <= n < m). - apply lt_wf. - intros x y; split. + intro H; split; [apply le_0_l | assumption]. + now intros [_ H]. Defined.
imports: NAdd