proposition: Lemma wf_stat_order : well_founded stat_order.
proof: Proof. unfold stat_order in |- *; apply well_founded_ltof. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid shift Compare_dec imperative while two_power log2_spec