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