helm/software/matita/contribs/didactic/induction_support.ma

   1 include "nat/minus.ma".
   2
   3 definition max : nat → nat → nat ≝
   4  λa,b:nat.
   5  let rec max n m on n ≝
   6   match n with
   7   [ O ⇒ b
   8   | S n ⇒
   9       match m with
  10       [ O ⇒ a
  11       | S m ⇒ max n m]]
  12  in
  13    max a b.
  14
  15 definition min : nat → nat → nat ≝
  16  λa,b:nat.
  17  let rec min n m on n ≝
  18   match n with
  19   [ O ⇒ a
  20   | S n ⇒
  21       match m with
  22       [ O ⇒ b
  23       | S m ⇒ min n m]]
  24  in
  25    min a b.