proposition: Theorem DisjLaLc : forall (a b : rNat) (Neqab : a <> b) (La Lb : list rZ) (Ar : rArray vM) (War : wellFormedArray Ar) (geta : rArrayGet _ Ar a = class La) (getb : rArrayGet _ Ar b = class Lb), DisjointRz La (appendRz (rZPlus b :: nil) Lb).
proof: Proof. intros a b ltab La Lb Ar War geta getb. cut (DisjointRz La Lb); [ intros DLaLb | apply wfDisjoint with (3 := geta) (4 := getb); auto with stalmarck ]. red in |- *; auto with stalmarck. apply DisjointCom; unfold appendRz in |- *; apply appendfDisjoint; auto with stalmarck. apply DisjbLb with (2 := getb); auto with stalmarck. apply DisjointDef; simpl in |- *; auto with stalmarck. intros a0 H'; inversion_clear H'. apply NotInEqComp with (a := rZPlus b); auto with stalmarck. apply wellFormedArrayInImpNotEq with (2 := getb) (3 := geta); auto with stalmarck. inversion_clear H. apply DisjointCom; auto with stalmarck. Qed.