helm/software/matita/contribs/RELATIONAL/NLE/inv.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/RELATIONAL/NLE/inv".
  16
  17 include "NLE/defs.ma".
  18
  19 theorem nle_inv_succ_1: \forall x,y. x < y \to
  20                         \exists z. y = succ z \land x <= z.
  21  intros. inversion H; clear H; intros; subst;
  22  [ destruct H
  23  | destruct H2. clear H2. subst. auto
  24  ]
  25 qed.
  26
  27 theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
  28  intros. inversion H; clear H; intros; subst;
  29  [ destruct H
  30  | destruct H2. destruct H3. clear H2 H3. subst. auto
  31  ]
  32 qed.
  33
  34 theorem nle_inv_succ_zero: \forall x. x < zero \to False.
  35  intros. inversion H; clear H; intros; subst;
  36  [ destruct H
  37  | destruct H3
  38  ]
  39 qed.
  40
  41 theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
  42  intros. inversion H; clear H; intros; subst;
  43  [ auto
  44  | destruct H3
  45  ].
  46 qed.
  47
  48 theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
  49                         x = zero \lor \exists z. x = succ z \land z <= y.
  50  intros. inversion H; clear H; intros; subst;
  51  [ auto
  52  | destruct H3. clear H3. subst. auto depth = 4
  53  ].
  54 qed.