Indeed, there is no need to use explicit rewriting, just reduction. The reductions of
leb (S n) (S m)
to leb n m
and S n + m
to S (n+m)
, which suggest a simple proof by induction on p
.
Lemma L:
forall n m p : nat, (n <=? m) = true -> (p + n <=? p + m) = true.
Proof.
induction p; simpl.
- now intros ?.
- assumption.
Qed.