proposition: Proposition sub_leq_0 (n m : nat) : n <= m -> n - m = 0.
proof: Proof. intro l; induction l. - exact (sub_n_n n). - change (m.+1) with (1 + m). destruct n. + reflexivity. + destruct (nat_add_comm m 1). destruct (symmetric_paths _ _ (subsubadd n.+1 m 1)). destruct (symmetric_paths _ _ IHl). reflexivity. Defined.
imports: Basics Spaces.Nat.Core