matita/contribs/library_auto/auto/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/library_autobatch/nat/relevant_equations".
  16
  17 include "auto/nat/times.ma".
  18 include "auto/nat/minus.ma".
  19 include "auto/nat/gcd.ma".
  20 (* if gcd is compiled before this, the applys will take too much *)
  21
  22 theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
  23 intros.
  24 apply (trans_eq ? ? (p*(n+m)))
  25 [ apply sym_times
  26 | apply (trans_eq ? ? (p*n+p*m));autobatch
  27   (*[ apply distr_times_plus
  28   | apply eq_f2;
  29       apply sym_times
  30   ]*)
  31 ]
  32 qed.
  33
  34 theorem times_minus_l: \forall n,m,p:nat. (n-m)*p = n*p - m*p.
  35 intros.
  36 apply (trans_eq ? ? (p*(n-m)))
  37 [ apply sym_times
  38 | apply (trans_eq ? ? (p*n-p*m));autobatch
  39   (*[ apply distr_times_minus
  40   | apply eq_f2;
  41       apply sym_times
  42   ]*)
  43 ]
  44 qed.
  45
  46 theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) =
  47 n*p + n*q + m*p + m*q.
  48 intros.
  49 autobatch.
  50 (*apply (trans_eq nat ? ((n*(p+q) + m*(p+q))))
  51 [ apply times_plus_l
  52 | rewrite > distr_times_plus.
  53   rewrite > distr_times_plus.
  54   rewrite < assoc_plus.
  55   reflexivity
  56 ]*)
  57 qed.