Require Import Coq.Program.Program.

Inductive Bit: Set :=
  | Zer: Bit
  | One: Bit.

Inductive List (set1: Set): Set :=
  | Empt: List set1
  | Fill: set1 -> List set1 -> List set1.

Implicit Arguments Empt [[set1]].

Implicit Arguments Fill [[set1]].

Fixpoint meas {set1: Set} (list1: List set1): nat :=
  match list1 with
  | Empt => O
  | Fill _ list2 => S (meas list2)
  end.

Definition Nat: Set := List Bit.

Fixpoint Trim (nat1: Nat): Prop :=
  match nat1 with
  | Empt => True
  | Fill Zer Empt => False
  | Fill _ nat2 => Trim nat2
  end.

Theorem VEGC: Trim (Fill Zer Empt) = False.
Proof.
trivial.
Qed.

Theorem MCOW: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
Proof.
destruct bit1.
  destruct nat1 as [ | bit2 nat2].
    intro H1. rewrite VEGC in H1. contradiction.
    trivial.
  trivial.
Qed.

Fixpoint Pos (nat1: Nat): Prop :=
  match nat1 with
  | Empt => False
  | Fill Zer nat2 => Pos nat2
  | Fill One _ => True
  end.

Theorem NXJN: Pos Empt = False.
Proof.
trivial.
Qed.

Theorem ZJSN: forall nat1: Nat, Pos (Fill Zer nat1) = Pos nat1.
Proof.
trivial.
Qed.

Definition trim (nat1: Nat): Nat :=
  match nat1 with
  | Fill Zer Empt => Empt
  | _ => nat1
  end.

Program Fixpoint pred (nat1: Nat | Trim nat1 /\ Pos nat1) {measure (meas nat1)}: Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat3 => Fill One (pred nat3)
  | Fill One nat3 => trim (Fill Zer nat3)
  end.

Next Obligation.
rewrite NXJN in p. contradiction.
Qed.

Next Obligation.
apply MCOW in t. rewrite ZJSN in p. split.
  assumption.
  assumption.
Qed.

Theorem ZJBJ: forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1).
Proof.
destruct nat1 as [nat3 H1]. decompose [and] H1. induction nat3 as [ | bit1 nat4].
  rewrite NXJN in H0. contradiction.
  destruct bit1.