[ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
simplify in Hf:(? ? %);
assumption
- | autobatch
+ | apply le_times_r. apply H'.
]
qed.
rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
rewrite > divides_to_eq_mod_mod_mod;
[ reflexivity
- | autobatch
+ | apply (witness ? ? 16). reflexivity.
]
]
qed.
match plusbyte b1 b2 c with
[ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
].
- intros;
+ intros; elim daemon.
+ (*
unfold plusbyte;
generalize in match (plusex_ok (bl b1) (bl b2) c);
elim (plusex (bl b1) (bl b2) c);
rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
rewrite > H; clear H;
autobatch paramodulation.
+ *)
qed.
definition bpred ≝
rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
rewrite > H1;
- rewrite > div_times_ltO; [2: autobatch | ]
+ rewrite > lt_O_to_div_times; [2: autobatch | ]
lapply (eq_f ? ? (λx.x/16) ? ? H1);
- rewrite > div_times_ltO in Hletin; [2: autobatch | ]
+ rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
rewrite > eq_mod_times_n_m_m_O in Hletin1;
elim daemon