proposition: Theorem DisjbLb : forall (b : rNat) (Lb : list rZ) (Ar : rArray vM) (War : wellFormedArray Ar) (getb : rArrayGet _ Ar b = class Lb), DisjointRz (rZPlus b :: nil) Lb.
proof: Proof. intros b Lb Ar War getb; red in |- *; simpl in |- *. apply DisjointDef; simpl in |- *; auto with stalmarck. intros a H'; inversion_clear H'. apply NotInEqComp with (a := rZPlus b); auto with stalmarck. apply wellFormedArrayInImpNotEqSimpl with (1 := War); auto with stalmarck. inversion H. Qed.