proposition: Lemma extendFunrZEval : forall (g : rNat -> bool) (n : rNat) (p : rZ) (s : bool), rVlt p n -> rZEval (extendFun n g s) p = rZEval g p.
proof: Proof. intros g n p; case p; unfold rVlt in |- *; simpl in |- *; auto with stalmarck. intros r s H'. unfold extendFun in |- *. case (rltDec r n); auto with stalmarck. intros s0; case s0; auto with stalmarck. intros H'0; absurd (rlt n r); auto with stalmarck. apply rltAntiSym; auto with stalmarck. intros H'0; absurd (r = n); auto with stalmarck. apply rltDef2; auto with stalmarck. intros r s H'. unfold extendFun in |- *. case (rltDec r n); auto with stalmarck. intros s0; case s0; auto with stalmarck. intros H'0; absurd (rlt n r); auto with stalmarck. apply rltAntiSym; auto with stalmarck. intros H'0; absurd (r = n); auto with stalmarck. apply rltDef2; auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)