proposition: Proposition sub_leq_0_converse (n m : nat) : n - m = 0 -> n <= m.
proof: Proof. revert m; simple_induction n n IHn. - auto with nat. - intros m eq. destruct m. + simpl in eq. apply symmetric_paths in eq. contradiction (not_eq_O_S n eq). + simpl in eq. apply leq_S_n', IHn, eq. Defined.
imports: Basics Spaces.Nat.Core