Advertisement
tinyevil

Untitled

Jan 21st, 2018
192
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.76 KB | None | 0 0
  1. Theorem mult_plus_distr_r : forall n m p : nat,
  2. (n + m) * p = (n * p) + (m * p).
  3. Proof.
  4. intros n m p.
  5. induction p.
  6. Focus 2.
  7. rewrite (mult_comm (n+m) (S p)).
  8. rewrite (mult_comm n (S p)).
  9. rewrite (mult_comm m (S p)).
  10. simpl.
  11. rewrite (mult_comm p (n + m)).
  12. rewrite IHp.
  13. rewrite <- (plus_assoc n (p*n) (m + p * m)).
  14. rewrite (plus_comm (p * n) (m + p * m)).
  15. rewrite (plus_assoc n (m + p * m) (p * n)).
  16. rewrite (plus_assoc n m (p*m)).
  17. rewrite (mult_comm n p).
  18. rewrite (mult_comm m p).
  19. rewrite (plus_comm (p * n) (p * m)).
  20. rewrite (plus_assoc (n + m) (p*m) (p*n)).
  21. reflexivity.
  22.  
  23.  
  24.  
  25.  
  26.  
  27.  
  28. (* or just... *)
  29.  
  30. Require Import Omega.
  31. Theorem mult_plus_distr_r : forall n m p : nat,
  32. (n + m) * p = (n * p) + (m * p).
  33. Proof.
  34. induction p; try omega; intuition.
  35. Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement