proposition: Lemma step_decreases G H: step G H -> measure H < measure G.
proof: Proof. rewrite /measure. case; intros=>/=; by rewrite ?card_option ?card_sum ?card_unit ?card_void ?addSnnS ?addnS ?addn0. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)