proposition: Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
proof: Proof. assert (∀ p, prod_decode_snd (prod_encode_snd p) = Some p). { intros p'. by induction p'; simplify_option_eq. } assert (∀ p, prod_decode_snd (prod_encode_fst p) = None). { intros p'. by induction p'; simplify_option_eq. } revert q. by induction p; intros [?|?|]; simplify_option_eq. Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)