proposition: Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (pos_compare i j).
proof: Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; constructor. Qed.
imports: Coq(Arith NArith List RelationClasses)