proposition: Lemma fin_O : forall x : Z, (x >= 0)%Z -> legal x (mkconfig 0%Z).
proof: Proof. intros; apply rec2_princ with (P := fun x : Z => legal x (mkconfig 0%Z)). apply legal_x_x. intros; apply legal_divide; auto. intros; apply legal_decrement; auto. trivial. Qed.
imports: ZArith Omega