proposition: Lemma o_proof : order A o.
proof: Proof. unfold o; constructor; auto. unfold reflexive; auto. unfold transitive; intros n1 n2 n3 H1 H2; apply Nat.le_trans with n2; trivial. unfold antisymmetric; auto with arith. Qed.
imports: Coq(Setoid Relations Arith FunInd)