proposition: Lemma andTb p : true && p = p.
proof: Proof. Lemma andbT p : p && true = p. Lemma orbC p q : p || q = q || p. Goal forall p q, (p && q) || ( p && ~~ q) || (~~ p && q) || (~~ p && ~~ q). Goal forall p q r, (p || q) && r = r && (p || q). Goal forall n, n < n.+1. by []. Qed.
imports: mathcomp(all_ssreflect)