helm/matita/library/nat/relevant_equations.ma

   1 (**************************************************************************)
   2 (*       __                                                               *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/relevant_equations.ma".
  16
  17 include "nat/times.ma".
  18
  19 theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
  20 intros.
  21 apply trans_eq ? ? (p*(n+m)).
  22 apply sym_times.
  23 apply trans_eq ? ? (p*n+p*m).
  24 apply distr_times_plus.
  25 apply eq_f2.
  26 apply sym_times.
  27 apply sym_times.
  28 qed.
  29
  30 theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) =
  31 n*p + n*q + m*p + m*q.
  32 intros.
  33 apply trans_eq nat ? ((n*(p+q) + m*(p+q))).
  34 apply times_plus_l.
  35 rewrite > distr_times_plus.
  36 rewrite > distr_times_plus.
  37 rewrite < assoc_plus.reflexivity.
  38 qed.