proposition: Lemma Wf_Call_lt : well_founded Call_lt.
proof: Proof. apply wf_coarser with (ltof Call Call_measure). exact measure_compat. apply well_founded_ltof. Qed.
imports: monoid spec Constants machine Euclid Le_lt_compl euclid shift two_power log2_spec develop Arith Peano_dec Compare_dec strategies Mult_compl Wf_nat Wf_compl