proposition: Lemma sum_option_r {A B}: bij (A + option B) (option (A + B)).
proof: Proof. etransitivity. apply bij_sumC. etransitivity. apply sum_option_l. apply option_bij, bij_sumC. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)