proposition: Lemma andb_true_elim b c: b && c -> c = true.
proof: Proof. case: c. - by case: b. Restart. case: c; first by []. Restart. case:c; [by [] | by case: b]. Restart. by do ![done | apply: eqxx | case: b | case: c]. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)