proposition: Theorem le_minus_left : forall a b c : nat, b <= a -> c <= a -> c <= b -> a - b <= a - c.
proof: Proof. intros a b c H; generalize c; clear c; elim H. rewrite Nat.sub_diag; auto with arith. intros a' Hle Hrec c H1. inversion H1. intros H2; rewrite (le_minus_O _ _ H2). auto with arith. auto with *. Qed.