Skip to main content
added 2 characters in body
Source Link

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. 

Indeed, there is no need to use rewriting, just reduction 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. 

Indeed, there is no need to use explicit rewriting. The reductions of leb (S n) (S m)to leb n m and S n + m to S (n+m) 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. 
Source Link

Indeed, there is no need to use rewriting, just reduction 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.